MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(U11(X1, X2)) -> U11(active(X1), X2)
, active(U11(tt(), V1)) -> mark(U12(isNatList(V1)))
, active(U12(X)) -> U12(active(X))
, active(U12(tt())) -> mark(tt())
, active(isNatList(cons(V1, V2))) ->
mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
, active(isNatList(nil())) -> mark(tt())
, active(U21(X1, X2)) -> U21(active(X1), X2)
, active(U21(tt(), V1)) -> mark(U22(isNat(V1)))
, active(U22(X)) -> U22(active(X))
, active(U22(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(U31(X1, X2)) -> U31(active(X1), X2)
, active(U31(tt(), V)) -> mark(U32(isNatList(V)))
, active(U32(X)) -> U32(active(X))
, active(U32(tt())) -> mark(tt())
, active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3)
, active(U41(tt(), V1, V2)) -> mark(U42(isNat(V1), V2))
, active(U42(X1, X2)) -> U42(active(X1), X2)
, active(U42(tt(), V2)) -> mark(U43(isNatIList(V2)))
, active(U43(X)) -> U43(active(X))
, active(U43(tt())) -> mark(tt())
, active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V))
, active(isNatIList(zeros())) -> mark(tt())
, active(isNatIList(cons(V1, V2))) ->
mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
, active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3)
, active(U51(tt(), V1, V2)) -> mark(U52(isNat(V1), V2))
, active(U52(X1, X2)) -> U52(active(X1), X2)
, active(U52(tt(), V2)) -> mark(U53(isNatList(V2)))
, active(U53(X)) -> U53(active(X))
, active(U53(tt())) -> mark(tt())
, active(U61(X1, X2)) -> U61(active(X1), X2)
, active(U61(tt(), L)) -> mark(s(length(L)))
, active(s(X)) -> s(active(X))
, active(length(X)) -> length(active(X))
, active(length(cons(N, L))) ->
mark(U61(and(and(isNatList(L), isNatIListKind(L)),
and(isNat(N), isNatKind(N))),
L))
, active(length(nil())) -> mark(0())
, active(and(X1, X2)) -> and(active(X1), X2)
, active(and(tt(), X)) -> mark(X)
, active(isNatIListKind(zeros())) -> mark(tt())
, active(isNatIListKind(cons(V1, V2))) ->
mark(and(isNatKind(V1), isNatIListKind(V2)))
, active(isNatIListKind(nil())) -> mark(tt())
, active(isNatKind(0())) -> mark(tt())
, active(isNatKind(s(V1))) -> mark(isNatKind(V1))
, active(isNatKind(length(V1))) -> mark(isNatIListKind(V1))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, U11(mark(X1), X2) -> mark(U11(X1, X2))
, U11(ok(X1), ok(X2)) -> ok(U11(X1, X2))
, U12(mark(X)) -> mark(U12(X))
, U12(ok(X)) -> ok(U12(X))
, isNatList(ok(X)) -> ok(isNatList(X))
, U21(mark(X1), X2) -> mark(U21(X1, X2))
, U21(ok(X1), ok(X2)) -> ok(U21(X1, X2))
, U22(mark(X)) -> mark(U22(X))
, U22(ok(X)) -> ok(U22(X))
, isNat(ok(X)) -> ok(isNat(X))
, U31(mark(X1), X2) -> mark(U31(X1, X2))
, U31(ok(X1), ok(X2)) -> ok(U31(X1, X2))
, U32(mark(X)) -> mark(U32(X))
, U32(ok(X)) -> ok(U32(X))
, U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3))
, U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3))
, U42(mark(X1), X2) -> mark(U42(X1, X2))
, U42(ok(X1), ok(X2)) -> ok(U42(X1, X2))
, U43(mark(X)) -> mark(U43(X))
, U43(ok(X)) -> ok(U43(X))
, isNatIList(ok(X)) -> ok(isNatIList(X))
, U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3))
, U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3))
, U52(mark(X1), X2) -> mark(U52(X1, X2))
, U52(ok(X1), ok(X2)) -> ok(U52(X1, X2))
, U53(mark(X)) -> mark(U53(X))
, U53(ok(X)) -> ok(U53(X))
, U61(mark(X1), X2) -> mark(U61(X1, X2))
, U61(ok(X1), ok(X2)) -> ok(U61(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))
, and(mark(X1), X2) -> mark(and(X1, X2))
, and(ok(X1), ok(X2)) -> ok(and(X1, X2))
, isNatIListKind(ok(X)) -> ok(isNatIListKind(X))
, isNatKind(ok(X)) -> ok(isNatKind(X))
, proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(U11(X1, X2)) -> U11(proper(X1), proper(X2))
, proper(tt()) -> ok(tt())
, proper(U12(X)) -> U12(proper(X))
, proper(isNatList(X)) -> isNatList(proper(X))
, proper(U21(X1, X2)) -> U21(proper(X1), proper(X2))
, proper(U22(X)) -> U22(proper(X))
, proper(isNat(X)) -> isNat(proper(X))
, proper(U31(X1, X2)) -> U31(proper(X1), proper(X2))
, proper(U32(X)) -> U32(proper(X))
, proper(U41(X1, X2, X3)) ->
U41(proper(X1), proper(X2), proper(X3))
, proper(U42(X1, X2)) -> U42(proper(X1), proper(X2))
, proper(U43(X)) -> U43(proper(X))
, proper(isNatIList(X)) -> isNatIList(proper(X))
, proper(U51(X1, X2, X3)) ->
U51(proper(X1), proper(X2), proper(X3))
, proper(U52(X1, X2)) -> U52(proper(X1), proper(X2))
, proper(U53(X)) -> U53(proper(X))
, proper(U61(X1, X2)) -> U61(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(length(X)) -> length(proper(X))
, proper(and(X1, X2)) -> and(proper(X1), proper(X2))
, proper(isNatIListKind(X)) -> isNatIListKind(proper(X))
, proper(isNatKind(X)) -> isNatKind(proper(X))
, proper(nil()) -> ok(nil())
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X)) }
Obligation:
runtime complexity
Answer:
MAYBE
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
following reason:
Computation stopped due to timeout after 60.0 seconds.
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
failed due to the following reason:
Computation stopped due to timeout after 30.0 seconds.
2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Bounds with perSymbol-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with minimal-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
3) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
to the following reason:
The processor is inapplicable, reason:
Processor only applicable for innermost runtime complexity analysis
2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
following reason:
The processor is inapplicable, reason:
Processor only applicable for innermost runtime complexity analysis
3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
due to the following reason:
We add the following weak dependency pairs:
Strict DPs:
{ active^#(zeros()) -> c_1(cons^#(0(), zeros()))
, active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2))
, active^#(U11(tt(), V1)) -> c_4(U12^#(isNatList(V1)))
, active^#(U12(X)) -> c_5(U12^#(active(X)))
, active^#(U12(tt())) -> c_6()
, active^#(isNatList(cons(V1, V2))) ->
c_7(U51^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
, active^#(isNatList(nil())) -> c_8()
, active^#(U21(X1, X2)) -> c_9(U21^#(active(X1), X2))
, active^#(U21(tt(), V1)) -> c_10(U22^#(isNat(V1)))
, active^#(U22(X)) -> c_11(U22^#(active(X)))
, active^#(U22(tt())) -> c_12()
, active^#(isNat(0())) -> c_13()
, active^#(isNat(s(V1))) -> c_14(U21^#(isNatKind(V1), V1))
, active^#(isNat(length(V1))) ->
c_15(U11^#(isNatIListKind(V1), V1))
, active^#(U31(X1, X2)) -> c_16(U31^#(active(X1), X2))
, active^#(U31(tt(), V)) -> c_17(U32^#(isNatList(V)))
, active^#(U32(X)) -> c_18(U32^#(active(X)))
, active^#(U32(tt())) -> c_19()
, active^#(U41(X1, X2, X3)) -> c_20(U41^#(active(X1), X2, X3))
, active^#(U41(tt(), V1, V2)) -> c_21(U42^#(isNat(V1), V2))
, active^#(U42(X1, X2)) -> c_22(U42^#(active(X1), X2))
, active^#(U42(tt(), V2)) -> c_23(U43^#(isNatIList(V2)))
, active^#(U43(X)) -> c_24(U43^#(active(X)))
, active^#(U43(tt())) -> c_25()
, active^#(isNatIList(V)) -> c_26(U31^#(isNatIListKind(V), V))
, active^#(isNatIList(zeros())) -> c_27()
, active^#(isNatIList(cons(V1, V2))) ->
c_28(U41^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
, active^#(U51(X1, X2, X3)) -> c_29(U51^#(active(X1), X2, X3))
, active^#(U51(tt(), V1, V2)) -> c_30(U52^#(isNat(V1), V2))
, active^#(U52(X1, X2)) -> c_31(U52^#(active(X1), X2))
, active^#(U52(tt(), V2)) -> c_32(U53^#(isNatList(V2)))
, active^#(U53(X)) -> c_33(U53^#(active(X)))
, active^#(U53(tt())) -> c_34()
, active^#(U61(X1, X2)) -> c_35(U61^#(active(X1), X2))
, active^#(U61(tt(), L)) -> c_36(s^#(length(L)))
, active^#(s(X)) -> c_37(s^#(active(X)))
, active^#(length(X)) -> c_38(length^#(active(X)))
, active^#(length(cons(N, L))) ->
c_39(U61^#(and(and(isNatList(L), isNatIListKind(L)),
and(isNat(N), isNatKind(N))),
L))
, active^#(length(nil())) -> c_40()
, active^#(and(X1, X2)) -> c_41(and^#(active(X1), X2))
, active^#(and(tt(), X)) -> c_42(X)
, active^#(isNatIListKind(zeros())) -> c_43()
, active^#(isNatIListKind(cons(V1, V2))) ->
c_44(and^#(isNatKind(V1), isNatIListKind(V2)))
, active^#(isNatIListKind(nil())) -> c_45()
, active^#(isNatKind(0())) -> c_46()
, active^#(isNatKind(s(V1))) -> c_47(isNatKind^#(V1))
, active^#(isNatKind(length(V1))) -> c_48(isNatIListKind^#(V1))
, cons^#(mark(X1), X2) -> c_49(cons^#(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_50(cons^#(X1, X2))
, U11^#(mark(X1), X2) -> c_51(U11^#(X1, X2))
, U11^#(ok(X1), ok(X2)) -> c_52(U11^#(X1, X2))
, U12^#(mark(X)) -> c_53(U12^#(X))
, U12^#(ok(X)) -> c_54(U12^#(X))
, U51^#(mark(X1), X2, X3) -> c_72(U51^#(X1, X2, X3))
, U51^#(ok(X1), ok(X2), ok(X3)) -> c_73(U51^#(X1, X2, X3))
, U21^#(mark(X1), X2) -> c_56(U21^#(X1, X2))
, U21^#(ok(X1), ok(X2)) -> c_57(U21^#(X1, X2))
, U22^#(mark(X)) -> c_58(U22^#(X))
, U22^#(ok(X)) -> c_59(U22^#(X))
, U31^#(mark(X1), X2) -> c_61(U31^#(X1, X2))
, U31^#(ok(X1), ok(X2)) -> c_62(U31^#(X1, X2))
, U32^#(mark(X)) -> c_63(U32^#(X))
, U32^#(ok(X)) -> c_64(U32^#(X))
, U41^#(mark(X1), X2, X3) -> c_65(U41^#(X1, X2, X3))
, U41^#(ok(X1), ok(X2), ok(X3)) -> c_66(U41^#(X1, X2, X3))
, U42^#(mark(X1), X2) -> c_67(U42^#(X1, X2))
, U42^#(ok(X1), ok(X2)) -> c_68(U42^#(X1, X2))
, U43^#(mark(X)) -> c_69(U43^#(X))
, U43^#(ok(X)) -> c_70(U43^#(X))
, U52^#(mark(X1), X2) -> c_74(U52^#(X1, X2))
, U52^#(ok(X1), ok(X2)) -> c_75(U52^#(X1, X2))
, U53^#(mark(X)) -> c_76(U53^#(X))
, U53^#(ok(X)) -> c_77(U53^#(X))
, U61^#(mark(X1), X2) -> c_78(U61^#(X1, X2))
, U61^#(ok(X1), ok(X2)) -> c_79(U61^#(X1, X2))
, s^#(mark(X)) -> c_80(s^#(X))
, s^#(ok(X)) -> c_81(s^#(X))
, length^#(mark(X)) -> c_82(length^#(X))
, length^#(ok(X)) -> c_83(length^#(X))
, and^#(mark(X1), X2) -> c_84(and^#(X1, X2))
, and^#(ok(X1), ok(X2)) -> c_85(and^#(X1, X2))
, isNatKind^#(ok(X)) -> c_87(isNatKind^#(X))
, isNatIListKind^#(ok(X)) -> c_86(isNatIListKind^#(X))
, isNatList^#(ok(X)) -> c_55(isNatList^#(X))
, isNat^#(ok(X)) -> c_60(isNat^#(X))
, isNatIList^#(ok(X)) -> c_71(isNatIList^#(X))
, proper^#(zeros()) -> c_88()
, proper^#(cons(X1, X2)) -> c_89(cons^#(proper(X1), proper(X2)))
, proper^#(0()) -> c_90()
, proper^#(U11(X1, X2)) -> c_91(U11^#(proper(X1), proper(X2)))
, proper^#(tt()) -> c_92()
, proper^#(U12(X)) -> c_93(U12^#(proper(X)))
, proper^#(isNatList(X)) -> c_94(isNatList^#(proper(X)))
, proper^#(U21(X1, X2)) -> c_95(U21^#(proper(X1), proper(X2)))
, proper^#(U22(X)) -> c_96(U22^#(proper(X)))
, proper^#(isNat(X)) -> c_97(isNat^#(proper(X)))
, proper^#(U31(X1, X2)) -> c_98(U31^#(proper(X1), proper(X2)))
, proper^#(U32(X)) -> c_99(U32^#(proper(X)))
, proper^#(U41(X1, X2, X3)) ->
c_100(U41^#(proper(X1), proper(X2), proper(X3)))
, proper^#(U42(X1, X2)) -> c_101(U42^#(proper(X1), proper(X2)))
, proper^#(U43(X)) -> c_102(U43^#(proper(X)))
, proper^#(isNatIList(X)) -> c_103(isNatIList^#(proper(X)))
, proper^#(U51(X1, X2, X3)) ->
c_104(U51^#(proper(X1), proper(X2), proper(X3)))
, proper^#(U52(X1, X2)) -> c_105(U52^#(proper(X1), proper(X2)))
, proper^#(U53(X)) -> c_106(U53^#(proper(X)))
, proper^#(U61(X1, X2)) -> c_107(U61^#(proper(X1), proper(X2)))
, proper^#(s(X)) -> c_108(s^#(proper(X)))
, proper^#(length(X)) -> c_109(length^#(proper(X)))
, proper^#(and(X1, X2)) -> c_110(and^#(proper(X1), proper(X2)))
, proper^#(isNatIListKind(X)) -> c_111(isNatIListKind^#(proper(X)))
, proper^#(isNatKind(X)) -> c_112(isNatKind^#(proper(X)))
, proper^#(nil()) -> c_113()
, top^#(mark(X)) -> c_114(top^#(proper(X)))
, top^#(ok(X)) -> c_115(top^#(active(X))) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ active^#(zeros()) -> c_1(cons^#(0(), zeros()))
, active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2))
, active^#(U11(tt(), V1)) -> c_4(U12^#(isNatList(V1)))
, active^#(U12(X)) -> c_5(U12^#(active(X)))
, active^#(U12(tt())) -> c_6()
, active^#(isNatList(cons(V1, V2))) ->
c_7(U51^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
, active^#(isNatList(nil())) -> c_8()
, active^#(U21(X1, X2)) -> c_9(U21^#(active(X1), X2))
, active^#(U21(tt(), V1)) -> c_10(U22^#(isNat(V1)))
, active^#(U22(X)) -> c_11(U22^#(active(X)))
, active^#(U22(tt())) -> c_12()
, active^#(isNat(0())) -> c_13()
, active^#(isNat(s(V1))) -> c_14(U21^#(isNatKind(V1), V1))
, active^#(isNat(length(V1))) ->
c_15(U11^#(isNatIListKind(V1), V1))
, active^#(U31(X1, X2)) -> c_16(U31^#(active(X1), X2))
, active^#(U31(tt(), V)) -> c_17(U32^#(isNatList(V)))
, active^#(U32(X)) -> c_18(U32^#(active(X)))
, active^#(U32(tt())) -> c_19()
, active^#(U41(X1, X2, X3)) -> c_20(U41^#(active(X1), X2, X3))
, active^#(U41(tt(), V1, V2)) -> c_21(U42^#(isNat(V1), V2))
, active^#(U42(X1, X2)) -> c_22(U42^#(active(X1), X2))
, active^#(U42(tt(), V2)) -> c_23(U43^#(isNatIList(V2)))
, active^#(U43(X)) -> c_24(U43^#(active(X)))
, active^#(U43(tt())) -> c_25()
, active^#(isNatIList(V)) -> c_26(U31^#(isNatIListKind(V), V))
, active^#(isNatIList(zeros())) -> c_27()
, active^#(isNatIList(cons(V1, V2))) ->
c_28(U41^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
, active^#(U51(X1, X2, X3)) -> c_29(U51^#(active(X1), X2, X3))
, active^#(U51(tt(), V1, V2)) -> c_30(U52^#(isNat(V1), V2))
, active^#(U52(X1, X2)) -> c_31(U52^#(active(X1), X2))
, active^#(U52(tt(), V2)) -> c_32(U53^#(isNatList(V2)))
, active^#(U53(X)) -> c_33(U53^#(active(X)))
, active^#(U53(tt())) -> c_34()
, active^#(U61(X1, X2)) -> c_35(U61^#(active(X1), X2))
, active^#(U61(tt(), L)) -> c_36(s^#(length(L)))
, active^#(s(X)) -> c_37(s^#(active(X)))
, active^#(length(X)) -> c_38(length^#(active(X)))
, active^#(length(cons(N, L))) ->
c_39(U61^#(and(and(isNatList(L), isNatIListKind(L)),
and(isNat(N), isNatKind(N))),
L))
, active^#(length(nil())) -> c_40()
, active^#(and(X1, X2)) -> c_41(and^#(active(X1), X2))
, active^#(and(tt(), X)) -> c_42(X)
, active^#(isNatIListKind(zeros())) -> c_43()
, active^#(isNatIListKind(cons(V1, V2))) ->
c_44(and^#(isNatKind(V1), isNatIListKind(V2)))
, active^#(isNatIListKind(nil())) -> c_45()
, active^#(isNatKind(0())) -> c_46()
, active^#(isNatKind(s(V1))) -> c_47(isNatKind^#(V1))
, active^#(isNatKind(length(V1))) -> c_48(isNatIListKind^#(V1))
, cons^#(mark(X1), X2) -> c_49(cons^#(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_50(cons^#(X1, X2))
, U11^#(mark(X1), X2) -> c_51(U11^#(X1, X2))
, U11^#(ok(X1), ok(X2)) -> c_52(U11^#(X1, X2))
, U12^#(mark(X)) -> c_53(U12^#(X))
, U12^#(ok(X)) -> c_54(U12^#(X))
, U51^#(mark(X1), X2, X3) -> c_72(U51^#(X1, X2, X3))
, U51^#(ok(X1), ok(X2), ok(X3)) -> c_73(U51^#(X1, X2, X3))
, U21^#(mark(X1), X2) -> c_56(U21^#(X1, X2))
, U21^#(ok(X1), ok(X2)) -> c_57(U21^#(X1, X2))
, U22^#(mark(X)) -> c_58(U22^#(X))
, U22^#(ok(X)) -> c_59(U22^#(X))
, U31^#(mark(X1), X2) -> c_61(U31^#(X1, X2))
, U31^#(ok(X1), ok(X2)) -> c_62(U31^#(X1, X2))
, U32^#(mark(X)) -> c_63(U32^#(X))
, U32^#(ok(X)) -> c_64(U32^#(X))
, U41^#(mark(X1), X2, X3) -> c_65(U41^#(X1, X2, X3))
, U41^#(ok(X1), ok(X2), ok(X3)) -> c_66(U41^#(X1, X2, X3))
, U42^#(mark(X1), X2) -> c_67(U42^#(X1, X2))
, U42^#(ok(X1), ok(X2)) -> c_68(U42^#(X1, X2))
, U43^#(mark(X)) -> c_69(U43^#(X))
, U43^#(ok(X)) -> c_70(U43^#(X))
, U52^#(mark(X1), X2) -> c_74(U52^#(X1, X2))
, U52^#(ok(X1), ok(X2)) -> c_75(U52^#(X1, X2))
, U53^#(mark(X)) -> c_76(U53^#(X))
, U53^#(ok(X)) -> c_77(U53^#(X))
, U61^#(mark(X1), X2) -> c_78(U61^#(X1, X2))
, U61^#(ok(X1), ok(X2)) -> c_79(U61^#(X1, X2))
, s^#(mark(X)) -> c_80(s^#(X))
, s^#(ok(X)) -> c_81(s^#(X))
, length^#(mark(X)) -> c_82(length^#(X))
, length^#(ok(X)) -> c_83(length^#(X))
, and^#(mark(X1), X2) -> c_84(and^#(X1, X2))
, and^#(ok(X1), ok(X2)) -> c_85(and^#(X1, X2))
, isNatKind^#(ok(X)) -> c_87(isNatKind^#(X))
, isNatIListKind^#(ok(X)) -> c_86(isNatIListKind^#(X))
, isNatList^#(ok(X)) -> c_55(isNatList^#(X))
, isNat^#(ok(X)) -> c_60(isNat^#(X))
, isNatIList^#(ok(X)) -> c_71(isNatIList^#(X))
, proper^#(zeros()) -> c_88()
, proper^#(cons(X1, X2)) -> c_89(cons^#(proper(X1), proper(X2)))
, proper^#(0()) -> c_90()
, proper^#(U11(X1, X2)) -> c_91(U11^#(proper(X1), proper(X2)))
, proper^#(tt()) -> c_92()
, proper^#(U12(X)) -> c_93(U12^#(proper(X)))
, proper^#(isNatList(X)) -> c_94(isNatList^#(proper(X)))
, proper^#(U21(X1, X2)) -> c_95(U21^#(proper(X1), proper(X2)))
, proper^#(U22(X)) -> c_96(U22^#(proper(X)))
, proper^#(isNat(X)) -> c_97(isNat^#(proper(X)))
, proper^#(U31(X1, X2)) -> c_98(U31^#(proper(X1), proper(X2)))
, proper^#(U32(X)) -> c_99(U32^#(proper(X)))
, proper^#(U41(X1, X2, X3)) ->
c_100(U41^#(proper(X1), proper(X2), proper(X3)))
, proper^#(U42(X1, X2)) -> c_101(U42^#(proper(X1), proper(X2)))
, proper^#(U43(X)) -> c_102(U43^#(proper(X)))
, proper^#(isNatIList(X)) -> c_103(isNatIList^#(proper(X)))
, proper^#(U51(X1, X2, X3)) ->
c_104(U51^#(proper(X1), proper(X2), proper(X3)))
, proper^#(U52(X1, X2)) -> c_105(U52^#(proper(X1), proper(X2)))
, proper^#(U53(X)) -> c_106(U53^#(proper(X)))
, proper^#(U61(X1, X2)) -> c_107(U61^#(proper(X1), proper(X2)))
, proper^#(s(X)) -> c_108(s^#(proper(X)))
, proper^#(length(X)) -> c_109(length^#(proper(X)))
, proper^#(and(X1, X2)) -> c_110(and^#(proper(X1), proper(X2)))
, proper^#(isNatIListKind(X)) -> c_111(isNatIListKind^#(proper(X)))
, proper^#(isNatKind(X)) -> c_112(isNatKind^#(proper(X)))
, proper^#(nil()) -> c_113()
, top^#(mark(X)) -> c_114(top^#(proper(X)))
, top^#(ok(X)) -> c_115(top^#(active(X))) }
Strict Trs:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(U11(X1, X2)) -> U11(active(X1), X2)
, active(U11(tt(), V1)) -> mark(U12(isNatList(V1)))
, active(U12(X)) -> U12(active(X))
, active(U12(tt())) -> mark(tt())
, active(isNatList(cons(V1, V2))) ->
mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
, active(isNatList(nil())) -> mark(tt())
, active(U21(X1, X2)) -> U21(active(X1), X2)
, active(U21(tt(), V1)) -> mark(U22(isNat(V1)))
, active(U22(X)) -> U22(active(X))
, active(U22(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(U31(X1, X2)) -> U31(active(X1), X2)
, active(U31(tt(), V)) -> mark(U32(isNatList(V)))
, active(U32(X)) -> U32(active(X))
, active(U32(tt())) -> mark(tt())
, active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3)
, active(U41(tt(), V1, V2)) -> mark(U42(isNat(V1), V2))
, active(U42(X1, X2)) -> U42(active(X1), X2)
, active(U42(tt(), V2)) -> mark(U43(isNatIList(V2)))
, active(U43(X)) -> U43(active(X))
, active(U43(tt())) -> mark(tt())
, active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V))
, active(isNatIList(zeros())) -> mark(tt())
, active(isNatIList(cons(V1, V2))) ->
mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
, active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3)
, active(U51(tt(), V1, V2)) -> mark(U52(isNat(V1), V2))
, active(U52(X1, X2)) -> U52(active(X1), X2)
, active(U52(tt(), V2)) -> mark(U53(isNatList(V2)))
, active(U53(X)) -> U53(active(X))
, active(U53(tt())) -> mark(tt())
, active(U61(X1, X2)) -> U61(active(X1), X2)
, active(U61(tt(), L)) -> mark(s(length(L)))
, active(s(X)) -> s(active(X))
, active(length(X)) -> length(active(X))
, active(length(cons(N, L))) ->
mark(U61(and(and(isNatList(L), isNatIListKind(L)),
and(isNat(N), isNatKind(N))),
L))
, active(length(nil())) -> mark(0())
, active(and(X1, X2)) -> and(active(X1), X2)
, active(and(tt(), X)) -> mark(X)
, active(isNatIListKind(zeros())) -> mark(tt())
, active(isNatIListKind(cons(V1, V2))) ->
mark(and(isNatKind(V1), isNatIListKind(V2)))
, active(isNatIListKind(nil())) -> mark(tt())
, active(isNatKind(0())) -> mark(tt())
, active(isNatKind(s(V1))) -> mark(isNatKind(V1))
, active(isNatKind(length(V1))) -> mark(isNatIListKind(V1))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, U11(mark(X1), X2) -> mark(U11(X1, X2))
, U11(ok(X1), ok(X2)) -> ok(U11(X1, X2))
, U12(mark(X)) -> mark(U12(X))
, U12(ok(X)) -> ok(U12(X))
, isNatList(ok(X)) -> ok(isNatList(X))
, U21(mark(X1), X2) -> mark(U21(X1, X2))
, U21(ok(X1), ok(X2)) -> ok(U21(X1, X2))
, U22(mark(X)) -> mark(U22(X))
, U22(ok(X)) -> ok(U22(X))
, isNat(ok(X)) -> ok(isNat(X))
, U31(mark(X1), X2) -> mark(U31(X1, X2))
, U31(ok(X1), ok(X2)) -> ok(U31(X1, X2))
, U32(mark(X)) -> mark(U32(X))
, U32(ok(X)) -> ok(U32(X))
, U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3))
, U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3))
, U42(mark(X1), X2) -> mark(U42(X1, X2))
, U42(ok(X1), ok(X2)) -> ok(U42(X1, X2))
, U43(mark(X)) -> mark(U43(X))
, U43(ok(X)) -> ok(U43(X))
, isNatIList(ok(X)) -> ok(isNatIList(X))
, U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3))
, U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3))
, U52(mark(X1), X2) -> mark(U52(X1, X2))
, U52(ok(X1), ok(X2)) -> ok(U52(X1, X2))
, U53(mark(X)) -> mark(U53(X))
, U53(ok(X)) -> ok(U53(X))
, U61(mark(X1), X2) -> mark(U61(X1, X2))
, U61(ok(X1), ok(X2)) -> ok(U61(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))
, and(mark(X1), X2) -> mark(and(X1, X2))
, and(ok(X1), ok(X2)) -> ok(and(X1, X2))
, isNatIListKind(ok(X)) -> ok(isNatIListKind(X))
, isNatKind(ok(X)) -> ok(isNatKind(X))
, proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(U11(X1, X2)) -> U11(proper(X1), proper(X2))
, proper(tt()) -> ok(tt())
, proper(U12(X)) -> U12(proper(X))
, proper(isNatList(X)) -> isNatList(proper(X))
, proper(U21(X1, X2)) -> U21(proper(X1), proper(X2))
, proper(U22(X)) -> U22(proper(X))
, proper(isNat(X)) -> isNat(proper(X))
, proper(U31(X1, X2)) -> U31(proper(X1), proper(X2))
, proper(U32(X)) -> U32(proper(X))
, proper(U41(X1, X2, X3)) ->
U41(proper(X1), proper(X2), proper(X3))
, proper(U42(X1, X2)) -> U42(proper(X1), proper(X2))
, proper(U43(X)) -> U43(proper(X))
, proper(isNatIList(X)) -> isNatIList(proper(X))
, proper(U51(X1, X2, X3)) ->
U51(proper(X1), proper(X2), proper(X3))
, proper(U52(X1, X2)) -> U52(proper(X1), proper(X2))
, proper(U53(X)) -> U53(proper(X))
, proper(U61(X1, X2)) -> U61(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(length(X)) -> length(proper(X))
, proper(and(X1, X2)) -> and(proper(X1), proper(X2))
, proper(isNatIListKind(X)) -> isNatIListKind(proper(X))
, proper(isNatKind(X)) -> isNatKind(proper(X))
, proper(nil()) -> ok(nil())
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X)) }
Obligation:
runtime complexity
Answer:
MAYBE
Consider the dependency graph:
1: active^#(zeros()) -> c_1(cons^#(0(), zeros()))
2: active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
-->_1 cons^#(ok(X1), ok(X2)) -> c_50(cons^#(X1, X2)) :50
-->_1 cons^#(mark(X1), X2) -> c_49(cons^#(X1, X2)) :49
3: active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2))
-->_1 U11^#(ok(X1), ok(X2)) -> c_52(U11^#(X1, X2)) :52
-->_1 U11^#(mark(X1), X2) -> c_51(U11^#(X1, X2)) :51
4: active^#(U11(tt(), V1)) -> c_4(U12^#(isNatList(V1)))
-->_1 U12^#(ok(X)) -> c_54(U12^#(X)) :54
-->_1 U12^#(mark(X)) -> c_53(U12^#(X)) :53
5: active^#(U12(X)) -> c_5(U12^#(active(X)))
-->_1 U12^#(ok(X)) -> c_54(U12^#(X)) :54
-->_1 U12^#(mark(X)) -> c_53(U12^#(X)) :53
6: active^#(U12(tt())) -> c_6()
7: active^#(isNatList(cons(V1, V2))) ->
c_7(U51^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
-->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_73(U51^#(X1, X2, X3)) :56
-->_1 U51^#(mark(X1), X2, X3) -> c_72(U51^#(X1, X2, X3)) :55
8: active^#(isNatList(nil())) -> c_8()
9: active^#(U21(X1, X2)) -> c_9(U21^#(active(X1), X2))
-->_1 U21^#(ok(X1), ok(X2)) -> c_57(U21^#(X1, X2)) :58
-->_1 U21^#(mark(X1), X2) -> c_56(U21^#(X1, X2)) :57
10: active^#(U21(tt(), V1)) -> c_10(U22^#(isNat(V1)))
-->_1 U22^#(ok(X)) -> c_59(U22^#(X)) :60
-->_1 U22^#(mark(X)) -> c_58(U22^#(X)) :59
11: active^#(U22(X)) -> c_11(U22^#(active(X)))
-->_1 U22^#(ok(X)) -> c_59(U22^#(X)) :60
-->_1 U22^#(mark(X)) -> c_58(U22^#(X)) :59
12: active^#(U22(tt())) -> c_12()
13: active^#(isNat(0())) -> c_13()
14: active^#(isNat(s(V1))) -> c_14(U21^#(isNatKind(V1), V1))
-->_1 U21^#(ok(X1), ok(X2)) -> c_57(U21^#(X1, X2)) :58
-->_1 U21^#(mark(X1), X2) -> c_56(U21^#(X1, X2)) :57
15: active^#(isNat(length(V1))) ->
c_15(U11^#(isNatIListKind(V1), V1))
-->_1 U11^#(ok(X1), ok(X2)) -> c_52(U11^#(X1, X2)) :52
-->_1 U11^#(mark(X1), X2) -> c_51(U11^#(X1, X2)) :51
16: active^#(U31(X1, X2)) -> c_16(U31^#(active(X1), X2))
-->_1 U31^#(ok(X1), ok(X2)) -> c_62(U31^#(X1, X2)) :62
-->_1 U31^#(mark(X1), X2) -> c_61(U31^#(X1, X2)) :61
17: active^#(U31(tt(), V)) -> c_17(U32^#(isNatList(V)))
-->_1 U32^#(ok(X)) -> c_64(U32^#(X)) :64
-->_1 U32^#(mark(X)) -> c_63(U32^#(X)) :63
18: active^#(U32(X)) -> c_18(U32^#(active(X)))
-->_1 U32^#(ok(X)) -> c_64(U32^#(X)) :64
-->_1 U32^#(mark(X)) -> c_63(U32^#(X)) :63
19: active^#(U32(tt())) -> c_19()
20: active^#(U41(X1, X2, X3)) -> c_20(U41^#(active(X1), X2, X3))
-->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_66(U41^#(X1, X2, X3)) :66
-->_1 U41^#(mark(X1), X2, X3) -> c_65(U41^#(X1, X2, X3)) :65
21: active^#(U41(tt(), V1, V2)) -> c_21(U42^#(isNat(V1), V2))
-->_1 U42^#(ok(X1), ok(X2)) -> c_68(U42^#(X1, X2)) :68
-->_1 U42^#(mark(X1), X2) -> c_67(U42^#(X1, X2)) :67
22: active^#(U42(X1, X2)) -> c_22(U42^#(active(X1), X2))
-->_1 U42^#(ok(X1), ok(X2)) -> c_68(U42^#(X1, X2)) :68
-->_1 U42^#(mark(X1), X2) -> c_67(U42^#(X1, X2)) :67
23: active^#(U42(tt(), V2)) -> c_23(U43^#(isNatIList(V2)))
-->_1 U43^#(ok(X)) -> c_70(U43^#(X)) :70
-->_1 U43^#(mark(X)) -> c_69(U43^#(X)) :69
24: active^#(U43(X)) -> c_24(U43^#(active(X)))
-->_1 U43^#(ok(X)) -> c_70(U43^#(X)) :70
-->_1 U43^#(mark(X)) -> c_69(U43^#(X)) :69
25: active^#(U43(tt())) -> c_25()
26: active^#(isNatIList(V)) -> c_26(U31^#(isNatIListKind(V), V))
-->_1 U31^#(ok(X1), ok(X2)) -> c_62(U31^#(X1, X2)) :62
-->_1 U31^#(mark(X1), X2) -> c_61(U31^#(X1, X2)) :61
27: active^#(isNatIList(zeros())) -> c_27()
28: active^#(isNatIList(cons(V1, V2))) ->
c_28(U41^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
-->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_66(U41^#(X1, X2, X3)) :66
-->_1 U41^#(mark(X1), X2, X3) -> c_65(U41^#(X1, X2, X3)) :65
29: active^#(U51(X1, X2, X3)) -> c_29(U51^#(active(X1), X2, X3))
-->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_73(U51^#(X1, X2, X3)) :56
-->_1 U51^#(mark(X1), X2, X3) -> c_72(U51^#(X1, X2, X3)) :55
30: active^#(U51(tt(), V1, V2)) -> c_30(U52^#(isNat(V1), V2))
-->_1 U52^#(ok(X1), ok(X2)) -> c_75(U52^#(X1, X2)) :72
-->_1 U52^#(mark(X1), X2) -> c_74(U52^#(X1, X2)) :71
31: active^#(U52(X1, X2)) -> c_31(U52^#(active(X1), X2))
-->_1 U52^#(ok(X1), ok(X2)) -> c_75(U52^#(X1, X2)) :72
-->_1 U52^#(mark(X1), X2) -> c_74(U52^#(X1, X2)) :71
32: active^#(U52(tt(), V2)) -> c_32(U53^#(isNatList(V2)))
-->_1 U53^#(ok(X)) -> c_77(U53^#(X)) :74
-->_1 U53^#(mark(X)) -> c_76(U53^#(X)) :73
33: active^#(U53(X)) -> c_33(U53^#(active(X)))
-->_1 U53^#(ok(X)) -> c_77(U53^#(X)) :74
-->_1 U53^#(mark(X)) -> c_76(U53^#(X)) :73
34: active^#(U53(tt())) -> c_34()
35: active^#(U61(X1, X2)) -> c_35(U61^#(active(X1), X2))
-->_1 U61^#(ok(X1), ok(X2)) -> c_79(U61^#(X1, X2)) :76
-->_1 U61^#(mark(X1), X2) -> c_78(U61^#(X1, X2)) :75
36: active^#(U61(tt(), L)) -> c_36(s^#(length(L)))
-->_1 s^#(ok(X)) -> c_81(s^#(X)) :78
-->_1 s^#(mark(X)) -> c_80(s^#(X)) :77
37: active^#(s(X)) -> c_37(s^#(active(X)))
-->_1 s^#(ok(X)) -> c_81(s^#(X)) :78
-->_1 s^#(mark(X)) -> c_80(s^#(X)) :77
38: active^#(length(X)) -> c_38(length^#(active(X)))
-->_1 length^#(ok(X)) -> c_83(length^#(X)) :80
-->_1 length^#(mark(X)) -> c_82(length^#(X)) :79
39: active^#(length(cons(N, L))) ->
c_39(U61^#(and(and(isNatList(L), isNatIListKind(L)),
and(isNat(N), isNatKind(N))),
L))
-->_1 U61^#(ok(X1), ok(X2)) -> c_79(U61^#(X1, X2)) :76
-->_1 U61^#(mark(X1), X2) -> c_78(U61^#(X1, X2)) :75
40: active^#(length(nil())) -> c_40()
41: active^#(and(X1, X2)) -> c_41(and^#(active(X1), X2))
-->_1 and^#(ok(X1), ok(X2)) -> c_85(and^#(X1, X2)) :82
-->_1 and^#(mark(X1), X2) -> c_84(and^#(X1, X2)) :81
42: active^#(and(tt(), X)) -> c_42(X)
-->_1 top^#(ok(X)) -> c_115(top^#(active(X))) :115
-->_1 top^#(mark(X)) -> c_114(top^#(proper(X))) :114
-->_1 proper^#(isNatKind(X)) -> c_112(isNatKind^#(proper(X))) :112
-->_1 proper^#(isNatIListKind(X)) ->
c_111(isNatIListKind^#(proper(X))) :111
-->_1 proper^#(and(X1, X2)) ->
c_110(and^#(proper(X1), proper(X2))) :110
-->_1 proper^#(length(X)) -> c_109(length^#(proper(X))) :109
-->_1 proper^#(s(X)) -> c_108(s^#(proper(X))) :108
-->_1 proper^#(U61(X1, X2)) ->
c_107(U61^#(proper(X1), proper(X2))) :107
-->_1 proper^#(U53(X)) -> c_106(U53^#(proper(X))) :106
-->_1 proper^#(U52(X1, X2)) ->
c_105(U52^#(proper(X1), proper(X2))) :105
-->_1 proper^#(U51(X1, X2, X3)) ->
c_104(U51^#(proper(X1), proper(X2), proper(X3))) :104
-->_1 proper^#(isNatIList(X)) ->
c_103(isNatIList^#(proper(X))) :103
-->_1 proper^#(U43(X)) -> c_102(U43^#(proper(X))) :102
-->_1 proper^#(U42(X1, X2)) ->
c_101(U42^#(proper(X1), proper(X2))) :101
-->_1 proper^#(U41(X1, X2, X3)) ->
c_100(U41^#(proper(X1), proper(X2), proper(X3))) :100
-->_1 proper^#(U32(X)) -> c_99(U32^#(proper(X))) :99
-->_1 proper^#(U31(X1, X2)) ->
c_98(U31^#(proper(X1), proper(X2))) :98
-->_1 proper^#(isNat(X)) -> c_97(isNat^#(proper(X))) :97
-->_1 proper^#(U22(X)) -> c_96(U22^#(proper(X))) :96
-->_1 proper^#(U21(X1, X2)) ->
c_95(U21^#(proper(X1), proper(X2))) :95
-->_1 proper^#(isNatList(X)) -> c_94(isNatList^#(proper(X))) :94
-->_1 proper^#(U12(X)) -> c_93(U12^#(proper(X))) :93
-->_1 proper^#(U11(X1, X2)) ->
c_91(U11^#(proper(X1), proper(X2))) :91
-->_1 proper^#(cons(X1, X2)) ->
c_89(cons^#(proper(X1), proper(X2))) :89
-->_1 isNatIList^#(ok(X)) -> c_71(isNatIList^#(X)) :87
-->_1 isNat^#(ok(X)) -> c_60(isNat^#(X)) :86
-->_1 isNatList^#(ok(X)) -> c_55(isNatList^#(X)) :85
-->_1 isNatIListKind^#(ok(X)) -> c_86(isNatIListKind^#(X)) :84
-->_1 isNatKind^#(ok(X)) -> c_87(isNatKind^#(X)) :83
-->_1 and^#(ok(X1), ok(X2)) -> c_85(and^#(X1, X2)) :82
-->_1 and^#(mark(X1), X2) -> c_84(and^#(X1, X2)) :81
-->_1 length^#(ok(X)) -> c_83(length^#(X)) :80
-->_1 length^#(mark(X)) -> c_82(length^#(X)) :79
-->_1 s^#(ok(X)) -> c_81(s^#(X)) :78
-->_1 s^#(mark(X)) -> c_80(s^#(X)) :77
-->_1 U61^#(ok(X1), ok(X2)) -> c_79(U61^#(X1, X2)) :76
-->_1 U61^#(mark(X1), X2) -> c_78(U61^#(X1, X2)) :75
-->_1 U53^#(ok(X)) -> c_77(U53^#(X)) :74
-->_1 U53^#(mark(X)) -> c_76(U53^#(X)) :73
-->_1 U52^#(ok(X1), ok(X2)) -> c_75(U52^#(X1, X2)) :72
-->_1 U52^#(mark(X1), X2) -> c_74(U52^#(X1, X2)) :71
-->_1 U43^#(ok(X)) -> c_70(U43^#(X)) :70
-->_1 U43^#(mark(X)) -> c_69(U43^#(X)) :69
-->_1 U42^#(ok(X1), ok(X2)) -> c_68(U42^#(X1, X2)) :68
-->_1 U42^#(mark(X1), X2) -> c_67(U42^#(X1, X2)) :67
-->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_66(U41^#(X1, X2, X3)) :66
-->_1 U41^#(mark(X1), X2, X3) -> c_65(U41^#(X1, X2, X3)) :65
-->_1 U32^#(ok(X)) -> c_64(U32^#(X)) :64
-->_1 U32^#(mark(X)) -> c_63(U32^#(X)) :63
-->_1 U31^#(ok(X1), ok(X2)) -> c_62(U31^#(X1, X2)) :62
-->_1 U31^#(mark(X1), X2) -> c_61(U31^#(X1, X2)) :61
-->_1 U22^#(ok(X)) -> c_59(U22^#(X)) :60
-->_1 U22^#(mark(X)) -> c_58(U22^#(X)) :59
-->_1 U21^#(ok(X1), ok(X2)) -> c_57(U21^#(X1, X2)) :58
-->_1 U21^#(mark(X1), X2) -> c_56(U21^#(X1, X2)) :57
-->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_73(U51^#(X1, X2, X3)) :56
-->_1 U51^#(mark(X1), X2, X3) -> c_72(U51^#(X1, X2, X3)) :55
-->_1 U12^#(ok(X)) -> c_54(U12^#(X)) :54
-->_1 U12^#(mark(X)) -> c_53(U12^#(X)) :53
-->_1 U11^#(ok(X1), ok(X2)) -> c_52(U11^#(X1, X2)) :52
-->_1 U11^#(mark(X1), X2) -> c_51(U11^#(X1, X2)) :51
-->_1 cons^#(ok(X1), ok(X2)) -> c_50(cons^#(X1, X2)) :50
-->_1 cons^#(mark(X1), X2) -> c_49(cons^#(X1, X2)) :49
-->_1 active^#(isNatKind(length(V1))) ->
c_48(isNatIListKind^#(V1)) :48
-->_1 active^#(isNatKind(s(V1))) -> c_47(isNatKind^#(V1)) :47
-->_1 active^#(isNatIListKind(cons(V1, V2))) ->
c_44(and^#(isNatKind(V1), isNatIListKind(V2))) :44
-->_1 proper^#(nil()) -> c_113() :113
-->_1 proper^#(tt()) -> c_92() :92
-->_1 proper^#(0()) -> c_90() :90
-->_1 proper^#(zeros()) -> c_88() :88
-->_1 active^#(isNatKind(0())) -> c_46() :46
-->_1 active^#(isNatIListKind(nil())) -> c_45() :45
-->_1 active^#(isNatIListKind(zeros())) -> c_43() :43
-->_1 active^#(and(tt(), X)) -> c_42(X) :42
-->_1 active^#(and(X1, X2)) -> c_41(and^#(active(X1), X2)) :41
-->_1 active^#(length(nil())) -> c_40() :40
-->_1 active^#(length(cons(N, L))) ->
c_39(U61^#(and(and(isNatList(L), isNatIListKind(L)),
and(isNat(N), isNatKind(N))),
L)) :39
-->_1 active^#(length(X)) -> c_38(length^#(active(X))) :38
-->_1 active^#(s(X)) -> c_37(s^#(active(X))) :37
-->_1 active^#(U61(tt(), L)) -> c_36(s^#(length(L))) :36
-->_1 active^#(U61(X1, X2)) -> c_35(U61^#(active(X1), X2)) :35
-->_1 active^#(U53(tt())) -> c_34() :34
-->_1 active^#(U53(X)) -> c_33(U53^#(active(X))) :33
-->_1 active^#(U52(tt(), V2)) -> c_32(U53^#(isNatList(V2))) :32
-->_1 active^#(U52(X1, X2)) -> c_31(U52^#(active(X1), X2)) :31
-->_1 active^#(U51(tt(), V1, V2)) -> c_30(U52^#(isNat(V1), V2)) :30
-->_1 active^#(U51(X1, X2, X3)) ->
c_29(U51^#(active(X1), X2, X3)) :29
-->_1 active^#(isNatIList(cons(V1, V2))) ->
c_28(U41^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) :28
-->_1 active^#(isNatIList(zeros())) -> c_27() :27
-->_1 active^#(isNatIList(V)) ->
c_26(U31^#(isNatIListKind(V), V)) :26
-->_1 active^#(U43(tt())) -> c_25() :25
-->_1 active^#(U43(X)) -> c_24(U43^#(active(X))) :24
-->_1 active^#(U42(tt(), V2)) -> c_23(U43^#(isNatIList(V2))) :23
-->_1 active^#(U42(X1, X2)) -> c_22(U42^#(active(X1), X2)) :22
-->_1 active^#(U41(tt(), V1, V2)) -> c_21(U42^#(isNat(V1), V2)) :21
-->_1 active^#(U41(X1, X2, X3)) ->
c_20(U41^#(active(X1), X2, X3)) :20
-->_1 active^#(U32(tt())) -> c_19() :19
-->_1 active^#(U32(X)) -> c_18(U32^#(active(X))) :18
-->_1 active^#(U31(tt(), V)) -> c_17(U32^#(isNatList(V))) :17
-->_1 active^#(U31(X1, X2)) -> c_16(U31^#(active(X1), X2)) :16
-->_1 active^#(isNat(length(V1))) ->
c_15(U11^#(isNatIListKind(V1), V1)) :15
-->_1 active^#(isNat(s(V1))) -> c_14(U21^#(isNatKind(V1), V1)) :14
-->_1 active^#(isNat(0())) -> c_13() :13
-->_1 active^#(U22(tt())) -> c_12() :12
-->_1 active^#(U22(X)) -> c_11(U22^#(active(X))) :11
-->_1 active^#(U21(tt(), V1)) -> c_10(U22^#(isNat(V1))) :10
-->_1 active^#(U21(X1, X2)) -> c_9(U21^#(active(X1), X2)) :9
-->_1 active^#(isNatList(nil())) -> c_8() :8
-->_1 active^#(isNatList(cons(V1, V2))) ->
c_7(U51^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) :7
-->_1 active^#(U12(tt())) -> c_6() :6
-->_1 active^#(U12(X)) -> c_5(U12^#(active(X))) :5
-->_1 active^#(U11(tt(), V1)) -> c_4(U12^#(isNatList(V1))) :4
-->_1 active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2)) :3
-->_1 active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) :2
-->_1 active^#(zeros()) -> c_1(cons^#(0(), zeros())) :1
43: active^#(isNatIListKind(zeros())) -> c_43()
44: active^#(isNatIListKind(cons(V1, V2))) ->
c_44(and^#(isNatKind(V1), isNatIListKind(V2)))
-->_1 and^#(ok(X1), ok(X2)) -> c_85(and^#(X1, X2)) :82
-->_1 and^#(mark(X1), X2) -> c_84(and^#(X1, X2)) :81
45: active^#(isNatIListKind(nil())) -> c_45()
46: active^#(isNatKind(0())) -> c_46()
47: active^#(isNatKind(s(V1))) -> c_47(isNatKind^#(V1))
-->_1 isNatKind^#(ok(X)) -> c_87(isNatKind^#(X)) :83
48: active^#(isNatKind(length(V1))) -> c_48(isNatIListKind^#(V1))
-->_1 isNatIListKind^#(ok(X)) -> c_86(isNatIListKind^#(X)) :84
49: cons^#(mark(X1), X2) -> c_49(cons^#(X1, X2))
-->_1 cons^#(ok(X1), ok(X2)) -> c_50(cons^#(X1, X2)) :50
-->_1 cons^#(mark(X1), X2) -> c_49(cons^#(X1, X2)) :49
50: cons^#(ok(X1), ok(X2)) -> c_50(cons^#(X1, X2))
-->_1 cons^#(ok(X1), ok(X2)) -> c_50(cons^#(X1, X2)) :50
-->_1 cons^#(mark(X1), X2) -> c_49(cons^#(X1, X2)) :49
51: U11^#(mark(X1), X2) -> c_51(U11^#(X1, X2))
-->_1 U11^#(ok(X1), ok(X2)) -> c_52(U11^#(X1, X2)) :52
-->_1 U11^#(mark(X1), X2) -> c_51(U11^#(X1, X2)) :51
52: U11^#(ok(X1), ok(X2)) -> c_52(U11^#(X1, X2))
-->_1 U11^#(ok(X1), ok(X2)) -> c_52(U11^#(X1, X2)) :52
-->_1 U11^#(mark(X1), X2) -> c_51(U11^#(X1, X2)) :51
53: U12^#(mark(X)) -> c_53(U12^#(X))
-->_1 U12^#(ok(X)) -> c_54(U12^#(X)) :54
-->_1 U12^#(mark(X)) -> c_53(U12^#(X)) :53
54: U12^#(ok(X)) -> c_54(U12^#(X))
-->_1 U12^#(ok(X)) -> c_54(U12^#(X)) :54
-->_1 U12^#(mark(X)) -> c_53(U12^#(X)) :53
55: U51^#(mark(X1), X2, X3) -> c_72(U51^#(X1, X2, X3))
-->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_73(U51^#(X1, X2, X3)) :56
-->_1 U51^#(mark(X1), X2, X3) -> c_72(U51^#(X1, X2, X3)) :55
56: U51^#(ok(X1), ok(X2), ok(X3)) -> c_73(U51^#(X1, X2, X3))
-->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_73(U51^#(X1, X2, X3)) :56
-->_1 U51^#(mark(X1), X2, X3) -> c_72(U51^#(X1, X2, X3)) :55
57: U21^#(mark(X1), X2) -> c_56(U21^#(X1, X2))
-->_1 U21^#(ok(X1), ok(X2)) -> c_57(U21^#(X1, X2)) :58
-->_1 U21^#(mark(X1), X2) -> c_56(U21^#(X1, X2)) :57
58: U21^#(ok(X1), ok(X2)) -> c_57(U21^#(X1, X2))
-->_1 U21^#(ok(X1), ok(X2)) -> c_57(U21^#(X1, X2)) :58
-->_1 U21^#(mark(X1), X2) -> c_56(U21^#(X1, X2)) :57
59: U22^#(mark(X)) -> c_58(U22^#(X))
-->_1 U22^#(ok(X)) -> c_59(U22^#(X)) :60
-->_1 U22^#(mark(X)) -> c_58(U22^#(X)) :59
60: U22^#(ok(X)) -> c_59(U22^#(X))
-->_1 U22^#(ok(X)) -> c_59(U22^#(X)) :60
-->_1 U22^#(mark(X)) -> c_58(U22^#(X)) :59
61: U31^#(mark(X1), X2) -> c_61(U31^#(X1, X2))
-->_1 U31^#(ok(X1), ok(X2)) -> c_62(U31^#(X1, X2)) :62
-->_1 U31^#(mark(X1), X2) -> c_61(U31^#(X1, X2)) :61
62: U31^#(ok(X1), ok(X2)) -> c_62(U31^#(X1, X2))
-->_1 U31^#(ok(X1), ok(X2)) -> c_62(U31^#(X1, X2)) :62
-->_1 U31^#(mark(X1), X2) -> c_61(U31^#(X1, X2)) :61
63: U32^#(mark(X)) -> c_63(U32^#(X))
-->_1 U32^#(ok(X)) -> c_64(U32^#(X)) :64
-->_1 U32^#(mark(X)) -> c_63(U32^#(X)) :63
64: U32^#(ok(X)) -> c_64(U32^#(X))
-->_1 U32^#(ok(X)) -> c_64(U32^#(X)) :64
-->_1 U32^#(mark(X)) -> c_63(U32^#(X)) :63
65: U41^#(mark(X1), X2, X3) -> c_65(U41^#(X1, X2, X3))
-->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_66(U41^#(X1, X2, X3)) :66
-->_1 U41^#(mark(X1), X2, X3) -> c_65(U41^#(X1, X2, X3)) :65
66: U41^#(ok(X1), ok(X2), ok(X3)) -> c_66(U41^#(X1, X2, X3))
-->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_66(U41^#(X1, X2, X3)) :66
-->_1 U41^#(mark(X1), X2, X3) -> c_65(U41^#(X1, X2, X3)) :65
67: U42^#(mark(X1), X2) -> c_67(U42^#(X1, X2))
-->_1 U42^#(ok(X1), ok(X2)) -> c_68(U42^#(X1, X2)) :68
-->_1 U42^#(mark(X1), X2) -> c_67(U42^#(X1, X2)) :67
68: U42^#(ok(X1), ok(X2)) -> c_68(U42^#(X1, X2))
-->_1 U42^#(ok(X1), ok(X2)) -> c_68(U42^#(X1, X2)) :68
-->_1 U42^#(mark(X1), X2) -> c_67(U42^#(X1, X2)) :67
69: U43^#(mark(X)) -> c_69(U43^#(X))
-->_1 U43^#(ok(X)) -> c_70(U43^#(X)) :70
-->_1 U43^#(mark(X)) -> c_69(U43^#(X)) :69
70: U43^#(ok(X)) -> c_70(U43^#(X))
-->_1 U43^#(ok(X)) -> c_70(U43^#(X)) :70
-->_1 U43^#(mark(X)) -> c_69(U43^#(X)) :69
71: U52^#(mark(X1), X2) -> c_74(U52^#(X1, X2))
-->_1 U52^#(ok(X1), ok(X2)) -> c_75(U52^#(X1, X2)) :72
-->_1 U52^#(mark(X1), X2) -> c_74(U52^#(X1, X2)) :71
72: U52^#(ok(X1), ok(X2)) -> c_75(U52^#(X1, X2))
-->_1 U52^#(ok(X1), ok(X2)) -> c_75(U52^#(X1, X2)) :72
-->_1 U52^#(mark(X1), X2) -> c_74(U52^#(X1, X2)) :71
73: U53^#(mark(X)) -> c_76(U53^#(X))
-->_1 U53^#(ok(X)) -> c_77(U53^#(X)) :74
-->_1 U53^#(mark(X)) -> c_76(U53^#(X)) :73
74: U53^#(ok(X)) -> c_77(U53^#(X))
-->_1 U53^#(ok(X)) -> c_77(U53^#(X)) :74
-->_1 U53^#(mark(X)) -> c_76(U53^#(X)) :73
75: U61^#(mark(X1), X2) -> c_78(U61^#(X1, X2))
-->_1 U61^#(ok(X1), ok(X2)) -> c_79(U61^#(X1, X2)) :76
-->_1 U61^#(mark(X1), X2) -> c_78(U61^#(X1, X2)) :75
76: U61^#(ok(X1), ok(X2)) -> c_79(U61^#(X1, X2))
-->_1 U61^#(ok(X1), ok(X2)) -> c_79(U61^#(X1, X2)) :76
-->_1 U61^#(mark(X1), X2) -> c_78(U61^#(X1, X2)) :75
77: s^#(mark(X)) -> c_80(s^#(X))
-->_1 s^#(ok(X)) -> c_81(s^#(X)) :78
-->_1 s^#(mark(X)) -> c_80(s^#(X)) :77
78: s^#(ok(X)) -> c_81(s^#(X))
-->_1 s^#(ok(X)) -> c_81(s^#(X)) :78
-->_1 s^#(mark(X)) -> c_80(s^#(X)) :77
79: length^#(mark(X)) -> c_82(length^#(X))
-->_1 length^#(ok(X)) -> c_83(length^#(X)) :80
-->_1 length^#(mark(X)) -> c_82(length^#(X)) :79
80: length^#(ok(X)) -> c_83(length^#(X))
-->_1 length^#(ok(X)) -> c_83(length^#(X)) :80
-->_1 length^#(mark(X)) -> c_82(length^#(X)) :79
81: and^#(mark(X1), X2) -> c_84(and^#(X1, X2))
-->_1 and^#(ok(X1), ok(X2)) -> c_85(and^#(X1, X2)) :82
-->_1 and^#(mark(X1), X2) -> c_84(and^#(X1, X2)) :81
82: and^#(ok(X1), ok(X2)) -> c_85(and^#(X1, X2))
-->_1 and^#(ok(X1), ok(X2)) -> c_85(and^#(X1, X2)) :82
-->_1 and^#(mark(X1), X2) -> c_84(and^#(X1, X2)) :81
83: isNatKind^#(ok(X)) -> c_87(isNatKind^#(X))
-->_1 isNatKind^#(ok(X)) -> c_87(isNatKind^#(X)) :83
84: isNatIListKind^#(ok(X)) -> c_86(isNatIListKind^#(X))
-->_1 isNatIListKind^#(ok(X)) -> c_86(isNatIListKind^#(X)) :84
85: isNatList^#(ok(X)) -> c_55(isNatList^#(X))
-->_1 isNatList^#(ok(X)) -> c_55(isNatList^#(X)) :85
86: isNat^#(ok(X)) -> c_60(isNat^#(X))
-->_1 isNat^#(ok(X)) -> c_60(isNat^#(X)) :86
87: isNatIList^#(ok(X)) -> c_71(isNatIList^#(X))
-->_1 isNatIList^#(ok(X)) -> c_71(isNatIList^#(X)) :87
88: proper^#(zeros()) -> c_88()
89: proper^#(cons(X1, X2)) -> c_89(cons^#(proper(X1), proper(X2)))
-->_1 cons^#(ok(X1), ok(X2)) -> c_50(cons^#(X1, X2)) :50
-->_1 cons^#(mark(X1), X2) -> c_49(cons^#(X1, X2)) :49
90: proper^#(0()) -> c_90()
91: proper^#(U11(X1, X2)) -> c_91(U11^#(proper(X1), proper(X2)))
-->_1 U11^#(ok(X1), ok(X2)) -> c_52(U11^#(X1, X2)) :52
-->_1 U11^#(mark(X1), X2) -> c_51(U11^#(X1, X2)) :51
92: proper^#(tt()) -> c_92()
93: proper^#(U12(X)) -> c_93(U12^#(proper(X)))
-->_1 U12^#(ok(X)) -> c_54(U12^#(X)) :54
-->_1 U12^#(mark(X)) -> c_53(U12^#(X)) :53
94: proper^#(isNatList(X)) -> c_94(isNatList^#(proper(X)))
-->_1 isNatList^#(ok(X)) -> c_55(isNatList^#(X)) :85
95: proper^#(U21(X1, X2)) -> c_95(U21^#(proper(X1), proper(X2)))
-->_1 U21^#(ok(X1), ok(X2)) -> c_57(U21^#(X1, X2)) :58
-->_1 U21^#(mark(X1), X2) -> c_56(U21^#(X1, X2)) :57
96: proper^#(U22(X)) -> c_96(U22^#(proper(X)))
-->_1 U22^#(ok(X)) -> c_59(U22^#(X)) :60
-->_1 U22^#(mark(X)) -> c_58(U22^#(X)) :59
97: proper^#(isNat(X)) -> c_97(isNat^#(proper(X)))
-->_1 isNat^#(ok(X)) -> c_60(isNat^#(X)) :86
98: proper^#(U31(X1, X2)) -> c_98(U31^#(proper(X1), proper(X2)))
-->_1 U31^#(ok(X1), ok(X2)) -> c_62(U31^#(X1, X2)) :62
-->_1 U31^#(mark(X1), X2) -> c_61(U31^#(X1, X2)) :61
99: proper^#(U32(X)) -> c_99(U32^#(proper(X)))
-->_1 U32^#(ok(X)) -> c_64(U32^#(X)) :64
-->_1 U32^#(mark(X)) -> c_63(U32^#(X)) :63
100: proper^#(U41(X1, X2, X3)) ->
c_100(U41^#(proper(X1), proper(X2), proper(X3)))
-->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_66(U41^#(X1, X2, X3)) :66
-->_1 U41^#(mark(X1), X2, X3) -> c_65(U41^#(X1, X2, X3)) :65
101: proper^#(U42(X1, X2)) -> c_101(U42^#(proper(X1), proper(X2)))
-->_1 U42^#(ok(X1), ok(X2)) -> c_68(U42^#(X1, X2)) :68
-->_1 U42^#(mark(X1), X2) -> c_67(U42^#(X1, X2)) :67
102: proper^#(U43(X)) -> c_102(U43^#(proper(X)))
-->_1 U43^#(ok(X)) -> c_70(U43^#(X)) :70
-->_1 U43^#(mark(X)) -> c_69(U43^#(X)) :69
103: proper^#(isNatIList(X)) -> c_103(isNatIList^#(proper(X)))
-->_1 isNatIList^#(ok(X)) -> c_71(isNatIList^#(X)) :87
104: proper^#(U51(X1, X2, X3)) ->
c_104(U51^#(proper(X1), proper(X2), proper(X3)))
-->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_73(U51^#(X1, X2, X3)) :56
-->_1 U51^#(mark(X1), X2, X3) -> c_72(U51^#(X1, X2, X3)) :55
105: proper^#(U52(X1, X2)) -> c_105(U52^#(proper(X1), proper(X2)))
-->_1 U52^#(ok(X1), ok(X2)) -> c_75(U52^#(X1, X2)) :72
-->_1 U52^#(mark(X1), X2) -> c_74(U52^#(X1, X2)) :71
106: proper^#(U53(X)) -> c_106(U53^#(proper(X)))
-->_1 U53^#(ok(X)) -> c_77(U53^#(X)) :74
-->_1 U53^#(mark(X)) -> c_76(U53^#(X)) :73
107: proper^#(U61(X1, X2)) -> c_107(U61^#(proper(X1), proper(X2)))
-->_1 U61^#(ok(X1), ok(X2)) -> c_79(U61^#(X1, X2)) :76
-->_1 U61^#(mark(X1), X2) -> c_78(U61^#(X1, X2)) :75
108: proper^#(s(X)) -> c_108(s^#(proper(X)))
-->_1 s^#(ok(X)) -> c_81(s^#(X)) :78
-->_1 s^#(mark(X)) -> c_80(s^#(X)) :77
109: proper^#(length(X)) -> c_109(length^#(proper(X)))
-->_1 length^#(ok(X)) -> c_83(length^#(X)) :80
-->_1 length^#(mark(X)) -> c_82(length^#(X)) :79
110: proper^#(and(X1, X2)) -> c_110(and^#(proper(X1), proper(X2)))
-->_1 and^#(ok(X1), ok(X2)) -> c_85(and^#(X1, X2)) :82
-->_1 and^#(mark(X1), X2) -> c_84(and^#(X1, X2)) :81
111: proper^#(isNatIListKind(X)) ->
c_111(isNatIListKind^#(proper(X)))
-->_1 isNatIListKind^#(ok(X)) -> c_86(isNatIListKind^#(X)) :84
112: proper^#(isNatKind(X)) -> c_112(isNatKind^#(proper(X)))
-->_1 isNatKind^#(ok(X)) -> c_87(isNatKind^#(X)) :83
113: proper^#(nil()) -> c_113()
114: top^#(mark(X)) -> c_114(top^#(proper(X)))
-->_1 top^#(ok(X)) -> c_115(top^#(active(X))) :115
-->_1 top^#(mark(X)) -> c_114(top^#(proper(X))) :114
115: top^#(ok(X)) -> c_115(top^#(active(X)))
-->_1 top^#(ok(X)) -> c_115(top^#(active(X))) :115
-->_1 top^#(mark(X)) -> c_114(top^#(proper(X))) :114
Only the nodes
{1,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,90,92,113,114,115}
are reachable from nodes
{1,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,90,92,113,114,115}
that start derivation from marked basic terms. The nodes not
reachable are removed from the problem.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ active^#(zeros()) -> c_1(cons^#(0(), zeros()))
, cons^#(mark(X1), X2) -> c_49(cons^#(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_50(cons^#(X1, X2))
, U11^#(mark(X1), X2) -> c_51(U11^#(X1, X2))
, U11^#(ok(X1), ok(X2)) -> c_52(U11^#(X1, X2))
, U12^#(mark(X)) -> c_53(U12^#(X))
, U12^#(ok(X)) -> c_54(U12^#(X))
, U51^#(mark(X1), X2, X3) -> c_72(U51^#(X1, X2, X3))
, U51^#(ok(X1), ok(X2), ok(X3)) -> c_73(U51^#(X1, X2, X3))
, U21^#(mark(X1), X2) -> c_56(U21^#(X1, X2))
, U21^#(ok(X1), ok(X2)) -> c_57(U21^#(X1, X2))
, U22^#(mark(X)) -> c_58(U22^#(X))
, U22^#(ok(X)) -> c_59(U22^#(X))
, U31^#(mark(X1), X2) -> c_61(U31^#(X1, X2))
, U31^#(ok(X1), ok(X2)) -> c_62(U31^#(X1, X2))
, U32^#(mark(X)) -> c_63(U32^#(X))
, U32^#(ok(X)) -> c_64(U32^#(X))
, U41^#(mark(X1), X2, X3) -> c_65(U41^#(X1, X2, X3))
, U41^#(ok(X1), ok(X2), ok(X3)) -> c_66(U41^#(X1, X2, X3))
, U42^#(mark(X1), X2) -> c_67(U42^#(X1, X2))
, U42^#(ok(X1), ok(X2)) -> c_68(U42^#(X1, X2))
, U43^#(mark(X)) -> c_69(U43^#(X))
, U43^#(ok(X)) -> c_70(U43^#(X))
, U52^#(mark(X1), X2) -> c_74(U52^#(X1, X2))
, U52^#(ok(X1), ok(X2)) -> c_75(U52^#(X1, X2))
, U53^#(mark(X)) -> c_76(U53^#(X))
, U53^#(ok(X)) -> c_77(U53^#(X))
, U61^#(mark(X1), X2) -> c_78(U61^#(X1, X2))
, U61^#(ok(X1), ok(X2)) -> c_79(U61^#(X1, X2))
, s^#(mark(X)) -> c_80(s^#(X))
, s^#(ok(X)) -> c_81(s^#(X))
, length^#(mark(X)) -> c_82(length^#(X))
, length^#(ok(X)) -> c_83(length^#(X))
, and^#(mark(X1), X2) -> c_84(and^#(X1, X2))
, and^#(ok(X1), ok(X2)) -> c_85(and^#(X1, X2))
, isNatKind^#(ok(X)) -> c_87(isNatKind^#(X))
, isNatIListKind^#(ok(X)) -> c_86(isNatIListKind^#(X))
, isNatList^#(ok(X)) -> c_55(isNatList^#(X))
, isNat^#(ok(X)) -> c_60(isNat^#(X))
, isNatIList^#(ok(X)) -> c_71(isNatIList^#(X))
, proper^#(zeros()) -> c_88()
, proper^#(0()) -> c_90()
, proper^#(tt()) -> c_92()
, proper^#(nil()) -> c_113()
, top^#(mark(X)) -> c_114(top^#(proper(X)))
, top^#(ok(X)) -> c_115(top^#(active(X))) }
Strict Trs:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(U11(X1, X2)) -> U11(active(X1), X2)
, active(U11(tt(), V1)) -> mark(U12(isNatList(V1)))
, active(U12(X)) -> U12(active(X))
, active(U12(tt())) -> mark(tt())
, active(isNatList(cons(V1, V2))) ->
mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
, active(isNatList(nil())) -> mark(tt())
, active(U21(X1, X2)) -> U21(active(X1), X2)
, active(U21(tt(), V1)) -> mark(U22(isNat(V1)))
, active(U22(X)) -> U22(active(X))
, active(U22(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(U31(X1, X2)) -> U31(active(X1), X2)
, active(U31(tt(), V)) -> mark(U32(isNatList(V)))
, active(U32(X)) -> U32(active(X))
, active(U32(tt())) -> mark(tt())
, active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3)
, active(U41(tt(), V1, V2)) -> mark(U42(isNat(V1), V2))
, active(U42(X1, X2)) -> U42(active(X1), X2)
, active(U42(tt(), V2)) -> mark(U43(isNatIList(V2)))
, active(U43(X)) -> U43(active(X))
, active(U43(tt())) -> mark(tt())
, active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V))
, active(isNatIList(zeros())) -> mark(tt())
, active(isNatIList(cons(V1, V2))) ->
mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
, active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3)
, active(U51(tt(), V1, V2)) -> mark(U52(isNat(V1), V2))
, active(U52(X1, X2)) -> U52(active(X1), X2)
, active(U52(tt(), V2)) -> mark(U53(isNatList(V2)))
, active(U53(X)) -> U53(active(X))
, active(U53(tt())) -> mark(tt())
, active(U61(X1, X2)) -> U61(active(X1), X2)
, active(U61(tt(), L)) -> mark(s(length(L)))
, active(s(X)) -> s(active(X))
, active(length(X)) -> length(active(X))
, active(length(cons(N, L))) ->
mark(U61(and(and(isNatList(L), isNatIListKind(L)),
and(isNat(N), isNatKind(N))),
L))
, active(length(nil())) -> mark(0())
, active(and(X1, X2)) -> and(active(X1), X2)
, active(and(tt(), X)) -> mark(X)
, active(isNatIListKind(zeros())) -> mark(tt())
, active(isNatIListKind(cons(V1, V2))) ->
mark(and(isNatKind(V1), isNatIListKind(V2)))
, active(isNatIListKind(nil())) -> mark(tt())
, active(isNatKind(0())) -> mark(tt())
, active(isNatKind(s(V1))) -> mark(isNatKind(V1))
, active(isNatKind(length(V1))) -> mark(isNatIListKind(V1))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, U11(mark(X1), X2) -> mark(U11(X1, X2))
, U11(ok(X1), ok(X2)) -> ok(U11(X1, X2))
, U12(mark(X)) -> mark(U12(X))
, U12(ok(X)) -> ok(U12(X))
, isNatList(ok(X)) -> ok(isNatList(X))
, U21(mark(X1), X2) -> mark(U21(X1, X2))
, U21(ok(X1), ok(X2)) -> ok(U21(X1, X2))
, U22(mark(X)) -> mark(U22(X))
, U22(ok(X)) -> ok(U22(X))
, isNat(ok(X)) -> ok(isNat(X))
, U31(mark(X1), X2) -> mark(U31(X1, X2))
, U31(ok(X1), ok(X2)) -> ok(U31(X1, X2))
, U32(mark(X)) -> mark(U32(X))
, U32(ok(X)) -> ok(U32(X))
, U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3))
, U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3))
, U42(mark(X1), X2) -> mark(U42(X1, X2))
, U42(ok(X1), ok(X2)) -> ok(U42(X1, X2))
, U43(mark(X)) -> mark(U43(X))
, U43(ok(X)) -> ok(U43(X))
, isNatIList(ok(X)) -> ok(isNatIList(X))
, U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3))
, U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3))
, U52(mark(X1), X2) -> mark(U52(X1, X2))
, U52(ok(X1), ok(X2)) -> ok(U52(X1, X2))
, U53(mark(X)) -> mark(U53(X))
, U53(ok(X)) -> ok(U53(X))
, U61(mark(X1), X2) -> mark(U61(X1, X2))
, U61(ok(X1), ok(X2)) -> ok(U61(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))
, and(mark(X1), X2) -> mark(and(X1, X2))
, and(ok(X1), ok(X2)) -> ok(and(X1, X2))
, isNatIListKind(ok(X)) -> ok(isNatIListKind(X))
, isNatKind(ok(X)) -> ok(isNatKind(X))
, proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(U11(X1, X2)) -> U11(proper(X1), proper(X2))
, proper(tt()) -> ok(tt())
, proper(U12(X)) -> U12(proper(X))
, proper(isNatList(X)) -> isNatList(proper(X))
, proper(U21(X1, X2)) -> U21(proper(X1), proper(X2))
, proper(U22(X)) -> U22(proper(X))
, proper(isNat(X)) -> isNat(proper(X))
, proper(U31(X1, X2)) -> U31(proper(X1), proper(X2))
, proper(U32(X)) -> U32(proper(X))
, proper(U41(X1, X2, X3)) ->
U41(proper(X1), proper(X2), proper(X3))
, proper(U42(X1, X2)) -> U42(proper(X1), proper(X2))
, proper(U43(X)) -> U43(proper(X))
, proper(isNatIList(X)) -> isNatIList(proper(X))
, proper(U51(X1, X2, X3)) ->
U51(proper(X1), proper(X2), proper(X3))
, proper(U52(X1, X2)) -> U52(proper(X1), proper(X2))
, proper(U53(X)) -> U53(proper(X))
, proper(U61(X1, X2)) -> U61(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(length(X)) -> length(proper(X))
, proper(and(X1, X2)) -> and(proper(X1), proper(X2))
, proper(isNatIListKind(X)) -> isNatIListKind(proper(X))
, proper(isNatKind(X)) -> isNatKind(proper(X))
, proper(nil()) -> ok(nil())
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X)) }
Obligation:
runtime complexity
Answer:
MAYBE
We estimate the number of application of {1,41,42,43,44} by
applications of Pre({1,41,42,43,44}) = {}. Here rules are labeled
as follows:
DPs:
{ 1: active^#(zeros()) -> c_1(cons^#(0(), zeros()))
, 2: cons^#(mark(X1), X2) -> c_49(cons^#(X1, X2))
, 3: cons^#(ok(X1), ok(X2)) -> c_50(cons^#(X1, X2))
, 4: U11^#(mark(X1), X2) -> c_51(U11^#(X1, X2))
, 5: U11^#(ok(X1), ok(X2)) -> c_52(U11^#(X1, X2))
, 6: U12^#(mark(X)) -> c_53(U12^#(X))
, 7: U12^#(ok(X)) -> c_54(U12^#(X))
, 8: U51^#(mark(X1), X2, X3) -> c_72(U51^#(X1, X2, X3))
, 9: U51^#(ok(X1), ok(X2), ok(X3)) -> c_73(U51^#(X1, X2, X3))
, 10: U21^#(mark(X1), X2) -> c_56(U21^#(X1, X2))
, 11: U21^#(ok(X1), ok(X2)) -> c_57(U21^#(X1, X2))
, 12: U22^#(mark(X)) -> c_58(U22^#(X))
, 13: U22^#(ok(X)) -> c_59(U22^#(X))
, 14: U31^#(mark(X1), X2) -> c_61(U31^#(X1, X2))
, 15: U31^#(ok(X1), ok(X2)) -> c_62(U31^#(X1, X2))
, 16: U32^#(mark(X)) -> c_63(U32^#(X))
, 17: U32^#(ok(X)) -> c_64(U32^#(X))
, 18: U41^#(mark(X1), X2, X3) -> c_65(U41^#(X1, X2, X3))
, 19: U41^#(ok(X1), ok(X2), ok(X3)) -> c_66(U41^#(X1, X2, X3))
, 20: U42^#(mark(X1), X2) -> c_67(U42^#(X1, X2))
, 21: U42^#(ok(X1), ok(X2)) -> c_68(U42^#(X1, X2))
, 22: U43^#(mark(X)) -> c_69(U43^#(X))
, 23: U43^#(ok(X)) -> c_70(U43^#(X))
, 24: U52^#(mark(X1), X2) -> c_74(U52^#(X1, X2))
, 25: U52^#(ok(X1), ok(X2)) -> c_75(U52^#(X1, X2))
, 26: U53^#(mark(X)) -> c_76(U53^#(X))
, 27: U53^#(ok(X)) -> c_77(U53^#(X))
, 28: U61^#(mark(X1), X2) -> c_78(U61^#(X1, X2))
, 29: U61^#(ok(X1), ok(X2)) -> c_79(U61^#(X1, X2))
, 30: s^#(mark(X)) -> c_80(s^#(X))
, 31: s^#(ok(X)) -> c_81(s^#(X))
, 32: length^#(mark(X)) -> c_82(length^#(X))
, 33: length^#(ok(X)) -> c_83(length^#(X))
, 34: and^#(mark(X1), X2) -> c_84(and^#(X1, X2))
, 35: and^#(ok(X1), ok(X2)) -> c_85(and^#(X1, X2))
, 36: isNatKind^#(ok(X)) -> c_87(isNatKind^#(X))
, 37: isNatIListKind^#(ok(X)) -> c_86(isNatIListKind^#(X))
, 38: isNatList^#(ok(X)) -> c_55(isNatList^#(X))
, 39: isNat^#(ok(X)) -> c_60(isNat^#(X))
, 40: isNatIList^#(ok(X)) -> c_71(isNatIList^#(X))
, 41: proper^#(zeros()) -> c_88()
, 42: proper^#(0()) -> c_90()
, 43: proper^#(tt()) -> c_92()
, 44: proper^#(nil()) -> c_113()
, 45: top^#(mark(X)) -> c_114(top^#(proper(X)))
, 46: top^#(ok(X)) -> c_115(top^#(active(X))) }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ cons^#(mark(X1), X2) -> c_49(cons^#(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_50(cons^#(X1, X2))
, U11^#(mark(X1), X2) -> c_51(U11^#(X1, X2))
, U11^#(ok(X1), ok(X2)) -> c_52(U11^#(X1, X2))
, U12^#(mark(X)) -> c_53(U12^#(X))
, U12^#(ok(X)) -> c_54(U12^#(X))
, U51^#(mark(X1), X2, X3) -> c_72(U51^#(X1, X2, X3))
, U51^#(ok(X1), ok(X2), ok(X3)) -> c_73(U51^#(X1, X2, X3))
, U21^#(mark(X1), X2) -> c_56(U21^#(X1, X2))
, U21^#(ok(X1), ok(X2)) -> c_57(U21^#(X1, X2))
, U22^#(mark(X)) -> c_58(U22^#(X))
, U22^#(ok(X)) -> c_59(U22^#(X))
, U31^#(mark(X1), X2) -> c_61(U31^#(X1, X2))
, U31^#(ok(X1), ok(X2)) -> c_62(U31^#(X1, X2))
, U32^#(mark(X)) -> c_63(U32^#(X))
, U32^#(ok(X)) -> c_64(U32^#(X))
, U41^#(mark(X1), X2, X3) -> c_65(U41^#(X1, X2, X3))
, U41^#(ok(X1), ok(X2), ok(X3)) -> c_66(U41^#(X1, X2, X3))
, U42^#(mark(X1), X2) -> c_67(U42^#(X1, X2))
, U42^#(ok(X1), ok(X2)) -> c_68(U42^#(X1, X2))
, U43^#(mark(X)) -> c_69(U43^#(X))
, U43^#(ok(X)) -> c_70(U43^#(X))
, U52^#(mark(X1), X2) -> c_74(U52^#(X1, X2))
, U52^#(ok(X1), ok(X2)) -> c_75(U52^#(X1, X2))
, U53^#(mark(X)) -> c_76(U53^#(X))
, U53^#(ok(X)) -> c_77(U53^#(X))
, U61^#(mark(X1), X2) -> c_78(U61^#(X1, X2))
, U61^#(ok(X1), ok(X2)) -> c_79(U61^#(X1, X2))
, s^#(mark(X)) -> c_80(s^#(X))
, s^#(ok(X)) -> c_81(s^#(X))
, length^#(mark(X)) -> c_82(length^#(X))
, length^#(ok(X)) -> c_83(length^#(X))
, and^#(mark(X1), X2) -> c_84(and^#(X1, X2))
, and^#(ok(X1), ok(X2)) -> c_85(and^#(X1, X2))
, isNatKind^#(ok(X)) -> c_87(isNatKind^#(X))
, isNatIListKind^#(ok(X)) -> c_86(isNatIListKind^#(X))
, isNatList^#(ok(X)) -> c_55(isNatList^#(X))
, isNat^#(ok(X)) -> c_60(isNat^#(X))
, isNatIList^#(ok(X)) -> c_71(isNatIList^#(X))
, top^#(mark(X)) -> c_114(top^#(proper(X)))
, top^#(ok(X)) -> c_115(top^#(active(X))) }
Strict Trs:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(U11(X1, X2)) -> U11(active(X1), X2)
, active(U11(tt(), V1)) -> mark(U12(isNatList(V1)))
, active(U12(X)) -> U12(active(X))
, active(U12(tt())) -> mark(tt())
, active(isNatList(cons(V1, V2))) ->
mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
, active(isNatList(nil())) -> mark(tt())
, active(U21(X1, X2)) -> U21(active(X1), X2)
, active(U21(tt(), V1)) -> mark(U22(isNat(V1)))
, active(U22(X)) -> U22(active(X))
, active(U22(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(U31(X1, X2)) -> U31(active(X1), X2)
, active(U31(tt(), V)) -> mark(U32(isNatList(V)))
, active(U32(X)) -> U32(active(X))
, active(U32(tt())) -> mark(tt())
, active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3)
, active(U41(tt(), V1, V2)) -> mark(U42(isNat(V1), V2))
, active(U42(X1, X2)) -> U42(active(X1), X2)
, active(U42(tt(), V2)) -> mark(U43(isNatIList(V2)))
, active(U43(X)) -> U43(active(X))
, active(U43(tt())) -> mark(tt())
, active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V))
, active(isNatIList(zeros())) -> mark(tt())
, active(isNatIList(cons(V1, V2))) ->
mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))
, active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3)
, active(U51(tt(), V1, V2)) -> mark(U52(isNat(V1), V2))
, active(U52(X1, X2)) -> U52(active(X1), X2)
, active(U52(tt(), V2)) -> mark(U53(isNatList(V2)))
, active(U53(X)) -> U53(active(X))
, active(U53(tt())) -> mark(tt())
, active(U61(X1, X2)) -> U61(active(X1), X2)
, active(U61(tt(), L)) -> mark(s(length(L)))
, active(s(X)) -> s(active(X))
, active(length(X)) -> length(active(X))
, active(length(cons(N, L))) ->
mark(U61(and(and(isNatList(L), isNatIListKind(L)),
and(isNat(N), isNatKind(N))),
L))
, active(length(nil())) -> mark(0())
, active(and(X1, X2)) -> and(active(X1), X2)
, active(and(tt(), X)) -> mark(X)
, active(isNatIListKind(zeros())) -> mark(tt())
, active(isNatIListKind(cons(V1, V2))) ->
mark(and(isNatKind(V1), isNatIListKind(V2)))
, active(isNatIListKind(nil())) -> mark(tt())
, active(isNatKind(0())) -> mark(tt())
, active(isNatKind(s(V1))) -> mark(isNatKind(V1))
, active(isNatKind(length(V1))) -> mark(isNatIListKind(V1))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, U11(mark(X1), X2) -> mark(U11(X1, X2))
, U11(ok(X1), ok(X2)) -> ok(U11(X1, X2))
, U12(mark(X)) -> mark(U12(X))
, U12(ok(X)) -> ok(U12(X))
, isNatList(ok(X)) -> ok(isNatList(X))
, U21(mark(X1), X2) -> mark(U21(X1, X2))
, U21(ok(X1), ok(X2)) -> ok(U21(X1, X2))
, U22(mark(X)) -> mark(U22(X))
, U22(ok(X)) -> ok(U22(X))
, isNat(ok(X)) -> ok(isNat(X))
, U31(mark(X1), X2) -> mark(U31(X1, X2))
, U31(ok(X1), ok(X2)) -> ok(U31(X1, X2))
, U32(mark(X)) -> mark(U32(X))
, U32(ok(X)) -> ok(U32(X))
, U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3))
, U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3))
, U42(mark(X1), X2) -> mark(U42(X1, X2))
, U42(ok(X1), ok(X2)) -> ok(U42(X1, X2))
, U43(mark(X)) -> mark(U43(X))
, U43(ok(X)) -> ok(U43(X))
, isNatIList(ok(X)) -> ok(isNatIList(X))
, U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3))
, U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3))
, U52(mark(X1), X2) -> mark(U52(X1, X2))
, U52(ok(X1), ok(X2)) -> ok(U52(X1, X2))
, U53(mark(X)) -> mark(U53(X))
, U53(ok(X)) -> ok(U53(X))
, U61(mark(X1), X2) -> mark(U61(X1, X2))
, U61(ok(X1), ok(X2)) -> ok(U61(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))
, and(mark(X1), X2) -> mark(and(X1, X2))
, and(ok(X1), ok(X2)) -> ok(and(X1, X2))
, isNatIListKind(ok(X)) -> ok(isNatIListKind(X))
, isNatKind(ok(X)) -> ok(isNatKind(X))
, proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(U11(X1, X2)) -> U11(proper(X1), proper(X2))
, proper(tt()) -> ok(tt())
, proper(U12(X)) -> U12(proper(X))
, proper(isNatList(X)) -> isNatList(proper(X))
, proper(U21(X1, X2)) -> U21(proper(X1), proper(X2))
, proper(U22(X)) -> U22(proper(X))
, proper(isNat(X)) -> isNat(proper(X))
, proper(U31(X1, X2)) -> U31(proper(X1), proper(X2))
, proper(U32(X)) -> U32(proper(X))
, proper(U41(X1, X2, X3)) ->
U41(proper(X1), proper(X2), proper(X3))
, proper(U42(X1, X2)) -> U42(proper(X1), proper(X2))
, proper(U43(X)) -> U43(proper(X))
, proper(isNatIList(X)) -> isNatIList(proper(X))
, proper(U51(X1, X2, X3)) ->
U51(proper(X1), proper(X2), proper(X3))
, proper(U52(X1, X2)) -> U52(proper(X1), proper(X2))
, proper(U53(X)) -> U53(proper(X))
, proper(U61(X1, X2)) -> U61(proper(X1), proper(X2))
, proper(s(X)) -> s(proper(X))
, proper(length(X)) -> length(proper(X))
, proper(and(X1, X2)) -> and(proper(X1), proper(X2))
, proper(isNatIListKind(X)) -> isNatIListKind(proper(X))
, proper(isNatKind(X)) -> isNatKind(proper(X))
, proper(nil()) -> ok(nil())
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X)) }
Weak DPs:
{ active^#(zeros()) -> c_1(cons^#(0(), zeros()))
, proper^#(zeros()) -> c_88()
, proper^#(0()) -> c_90()
, proper^#(tt()) -> c_92()
, proper^#(nil()) -> c_113() }
Obligation:
runtime complexity
Answer:
MAYBE
Empty strict component of the problem is NOT empty.
Arrrr..