MAYBE Time: 0.579290 TRS: { a__U12(X1, X2, X3) -> U12(X1, X2, X3), a__U12(tt(), V1, V2) -> a__U13(a__isNatKind V2, V1, V2), a__isNatKind X -> isNatKind X, a__isNatKind s V1 -> a__U41 a__isNatKind V1, a__isNatKind 0() -> tt(), a__isNatKind plus(V1, V2) -> a__U31(a__isNatKind V1, V2), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), V1, V2) -> a__U12(a__isNatKind V1, V1, V2), a__U13(X1, X2, X3) -> U13(X1, X2, X3), a__U13(tt(), V1, V2) -> a__U14(a__isNatKind V2, V1, V2), a__U14(X1, X2, X3) -> U14(X1, X2, X3), a__U14(tt(), V1, V2) -> a__U15(a__isNat V1, V2), a__U15(X1, X2) -> U15(X1, X2), a__U15(tt(), V2) -> a__U16 a__isNat V2, a__isNat X -> isNat X, a__isNat s V1 -> a__U21(a__isNatKind V1, V1), a__isNat 0() -> tt(), a__isNat plus(V1, V2) -> a__U11(a__isNatKind V1, V1, V2), a__U16 X -> U16 X, a__U16 tt() -> tt(), a__U22(X1, X2) -> U22(X1, X2), a__U22(tt(), V1) -> a__U23 a__isNat V1, a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22(a__isNatKind V1, V1), a__U23 X -> U23 X, a__U23 tt() -> tt(), a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V2) -> a__U32 a__isNatKind V2, a__U41 X -> U41 X, a__U41 tt() -> tt(), a__U52(X1, X2) -> U52(X1, X2), a__U52(tt(), N) -> mark N, a__U51(X1, X2) -> U51(X1, X2), a__U51(tt(), N) -> a__U52(a__isNatKind N, N), mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3), mark U12(X1, X2, X3) -> a__U12(mark X1, X2, X3), mark isNatKind X -> a__isNatKind X, mark U13(X1, X2, X3) -> a__U13(mark X1, X2, X3), mark U14(X1, X2, X3) -> a__U14(mark X1, X2, X3), mark U15(X1, X2) -> a__U15(mark X1, X2), mark isNat X -> a__isNat X, mark U16 X -> a__U16 mark X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22(X1, X2) -> a__U22(mark X1, X2), mark U23 X -> a__U23 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41 X -> a__U41 mark X, mark U51(X1, X2) -> a__U51(mark X1, X2), mark U52(X1, X2) -> a__U52(mark X1, X2), mark U61(X1, X2, X3) -> a__U61(mark X1, X2, X3), mark U62(X1, X2, X3) -> a__U62(mark X1, X2, X3), mark U63(X1, X2, X3) -> a__U63(mark X1, X2, X3), mark U64(X1, X2, X3) -> a__U64(mark X1, X2, X3), a__U62(X1, X2, X3) -> U62(X1, X2, X3), a__U62(tt(), M, N) -> a__U63(a__isNat N, M, N), a__U61(X1, X2, X3) -> U61(X1, X2, X3), a__U61(tt(), M, N) -> a__U62(a__isNatKind M, M, N), a__U63(X1, X2, X3) -> U63(X1, X2, X3), a__U63(tt(), M, N) -> a__U64(a__isNatKind N, M, N), a__U64(X1, X2, X3) -> U64(X1, X2, X3), a__U64(tt(), M, N) -> s a__plus(mark N, mark M), a__plus(N, s M) -> a__U61(a__isNat M, M, N), a__plus(N, 0()) -> a__U51(a__isNat N, N), a__plus(X1, X2) -> plus(X1, X2)} DP: DP: { a__U12#(tt(), V1, V2) -> a__isNatKind# V2, a__U12#(tt(), V1, V2) -> a__U13#(a__isNatKind V2, V1, V2), a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__U41# a__isNatKind V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2), a__U11#(tt(), V1, V2) -> a__U12#(a__isNatKind V1, V1, V2), a__U11#(tt(), V1, V2) -> a__isNatKind# V1, a__U13#(tt(), V1, V2) -> a__isNatKind# V2, a__U13#(tt(), V1, V2) -> a__U14#(a__isNatKind V2, V1, V2), a__U14#(tt(), V1, V2) -> a__U15#(a__isNat V1, V2), a__U14#(tt(), V1, V2) -> a__isNat# V1, a__U15#(tt(), V2) -> a__isNat# V2, a__U15#(tt(), V2) -> a__U16# a__isNat V2, a__isNat# s V1 -> a__isNatKind# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__isNat# plus(V1, V2) -> a__isNatKind# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNatKind V1, V1, V2), a__U22#(tt(), V1) -> a__isNat# V1, a__U22#(tt(), V1) -> a__U23# a__isNat V1, a__U21#(tt(), V1) -> a__isNatKind# V1, a__U21#(tt(), V1) -> a__U22#(a__isNatKind V1, V1), a__U31#(tt(), V2) -> a__isNatKind# V2, a__U31#(tt(), V2) -> a__U32# a__isNatKind V2, a__U52#(tt(), N) -> mark# N, a__U51#(tt(), N) -> a__isNatKind# N, a__U51#(tt(), N) -> a__U52#(a__isNatKind N, N), mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), mark# U12(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3), mark# U13(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3), mark# U14(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2), mark# U15(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X, mark# U16 X -> a__U16# mark X, mark# U16 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2), mark# U21(X1, X2) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2), mark# U22(X1, X2) -> mark# X1, mark# U23 X -> a__U23# mark X, mark# U23 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2), mark# U31(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X, mark# U32 X -> mark# X, mark# U41 X -> a__U41# mark X, mark# U41 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2), mark# U51(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2), mark# U52(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3), mark# U62(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3), mark# U63(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3), mark# U64(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3), a__U62#(tt(), M, N) -> a__isNat# N, a__U62#(tt(), M, N) -> a__U63#(a__isNat N, M, N), a__U61#(tt(), M, N) -> a__isNatKind# M, a__U61#(tt(), M, N) -> a__U62#(a__isNatKind M, M, N), a__U63#(tt(), M, N) -> a__isNatKind# N, a__U63#(tt(), M, N) -> a__U64#(a__isNatKind N, M, N), a__U64#(tt(), M, N) -> mark# N, a__U64#(tt(), M, N) -> mark# M, a__U64#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__isNat# M, a__plus#(N, s M) -> a__U61#(a__isNat M, M, N), a__plus#(N, 0()) -> a__isNat# N, a__plus#(N, 0()) -> a__U51#(a__isNat N, N)} TRS: { a__U12(X1, X2, X3) -> U12(X1, X2, X3), a__U12(tt(), V1, V2) -> a__U13(a__isNatKind V2, V1, V2), a__isNatKind X -> isNatKind X, a__isNatKind s V1 -> a__U41 a__isNatKind V1, a__isNatKind 0() -> tt(), a__isNatKind plus(V1, V2) -> a__U31(a__isNatKind V1, V2), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), V1, V2) -> a__U12(a__isNatKind V1, V1, V2), a__U13(X1, X2, X3) -> U13(X1, X2, X3), a__U13(tt(), V1, V2) -> a__U14(a__isNatKind V2, V1, V2), a__U14(X1, X2, X3) -> U14(X1, X2, X3), a__U14(tt(), V1, V2) -> a__U15(a__isNat V1, V2), a__U15(X1, X2) -> U15(X1, X2), a__U15(tt(), V2) -> a__U16 a__isNat V2, a__isNat X -> isNat X, a__isNat s V1 -> a__U21(a__isNatKind V1, V1), a__isNat 0() -> tt(), a__isNat plus(V1, V2) -> a__U11(a__isNatKind V1, V1, V2), a__U16 X -> U16 X, a__U16 tt() -> tt(), a__U22(X1, X2) -> U22(X1, X2), a__U22(tt(), V1) -> a__U23 a__isNat V1, a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22(a__isNatKind V1, V1), a__U23 X -> U23 X, a__U23 tt() -> tt(), a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V2) -> a__U32 a__isNatKind V2, a__U41 X -> U41 X, a__U41 tt() -> tt(), a__U52(X1, X2) -> U52(X1, X2), a__U52(tt(), N) -> mark N, a__U51(X1, X2) -> U51(X1, X2), a__U51(tt(), N) -> a__U52(a__isNatKind N, N), mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3), mark U12(X1, X2, X3) -> a__U12(mark X1, X2, X3), mark isNatKind X -> a__isNatKind X, mark U13(X1, X2, X3) -> a__U13(mark X1, X2, X3), mark U14(X1, X2, X3) -> a__U14(mark X1, X2, X3), mark U15(X1, X2) -> a__U15(mark X1, X2), mark isNat X -> a__isNat X, mark U16 X -> a__U16 mark X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22(X1, X2) -> a__U22(mark X1, X2), mark U23 X -> a__U23 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41 X -> a__U41 mark X, mark U51(X1, X2) -> a__U51(mark X1, X2), mark U52(X1, X2) -> a__U52(mark X1, X2), mark U61(X1, X2, X3) -> a__U61(mark X1, X2, X3), mark U62(X1, X2, X3) -> a__U62(mark X1, X2, X3), mark U63(X1, X2, X3) -> a__U63(mark X1, X2, X3), mark U64(X1, X2, X3) -> a__U64(mark X1, X2, X3), a__U62(X1, X2, X3) -> U62(X1, X2, X3), a__U62(tt(), M, N) -> a__U63(a__isNat N, M, N), a__U61(X1, X2, X3) -> U61(X1, X2, X3), a__U61(tt(), M, N) -> a__U62(a__isNatKind M, M, N), a__U63(X1, X2, X3) -> U63(X1, X2, X3), a__U63(tt(), M, N) -> a__U64(a__isNatKind N, M, N), a__U64(X1, X2, X3) -> U64(X1, X2, X3), a__U64(tt(), M, N) -> s a__plus(mark N, mark M), a__plus(N, s M) -> a__U61(a__isNat M, M, N), a__plus(N, 0()) -> a__U51(a__isNat N, N), a__plus(X1, X2) -> plus(X1, X2)} EDG: { (a__U64#(tt(), M, N) -> mark# M, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# M, mark# U64(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# M, mark# U63(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# M, mark# U62(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# M, mark# U61(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U52(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (a__U64#(tt(), M, N) -> mark# M, mark# U51(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (a__U64#(tt(), M, N) -> mark# M, mark# U41 X -> mark# X) (a__U64#(tt(), M, N) -> mark# M, mark# U41 X -> a__U41# mark X) (a__U64#(tt(), M, N) -> mark# M, mark# U32 X -> mark# X) (a__U64#(tt(), M, N) -> mark# M, mark# U32 X -> a__U32# mark X) (a__U64#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U64#(tt(), M, N) -> mark# M, mark# U23 X -> mark# X) (a__U64#(tt(), M, N) -> mark# M, mark# U23 X -> a__U23# mark X) (a__U64#(tt(), M, N) -> mark# M, mark# U22(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (a__U64#(tt(), M, N) -> mark# M, mark# U21(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U64#(tt(), M, N) -> mark# M, mark# U16 X -> mark# X) (a__U64#(tt(), M, N) -> mark# M, mark# U16 X -> a__U16# mark X) (a__U64#(tt(), M, N) -> mark# M, mark# isNat X -> a__isNat# X) (a__U64#(tt(), M, N) -> mark# M, mark# U15(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (a__U64#(tt(), M, N) -> mark# M, mark# U14(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# M, mark# U13(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# M, mark# isNatKind X -> a__isNatKind# X) (a__U64#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U64#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U64#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), V1, V2) -> a__isNatKind# V1) (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), V1, V2) -> a__U12#(a__isNatKind V1, V1, V2)) (mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3), a__U13#(tt(), V1, V2) -> a__U14#(a__isNatKind V2, V1, V2)) (mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3), a__U13#(tt(), V1, V2) -> a__isNatKind# V2) (mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3), a__U61#(tt(), M, N) -> a__U62#(a__isNatKind M, M, N)) (mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3), a__U61#(tt(), M, N) -> a__isNatKind# M) (mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3), a__U63#(tt(), M, N) -> a__U64#(a__isNatKind N, M, N)) (mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3), a__U63#(tt(), M, N) -> a__isNatKind# N) (a__U51#(tt(), N) -> a__U52#(a__isNatKind N, N), a__U52#(tt(), N) -> mark# N) (mark# plus(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U41 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U23 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U16 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# plus(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# plus(X1, X2) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U41 X -> mark# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U23 X -> mark# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U16 X -> mark# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U12(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U14(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U14(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U14(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U14(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U14(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U14(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U14(X1, X2, X3) -> mark# X1, mark# U41 X -> mark# X) (mark# U14(X1, X2, X3) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U14(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U14(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U14(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U14(X1, X2, X3) -> mark# X1, mark# U23 X -> mark# X) (mark# U14(X1, X2, X3) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U14(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U14(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U14(X1, X2, X3) -> mark# X1, mark# U16 X -> mark# X) (mark# U14(X1, X2, X3) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U14(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U14(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U14(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U14(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U14(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U14(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U14(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U14(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U14(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U14(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U14(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U41 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U23 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U16 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U21(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U21(X1, X2) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U21(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U41 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U23 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U16 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U31(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U31(X1, X2) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U31(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U31(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U31(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U52(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U52(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U52(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U52(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# U41 X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U52(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U52(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# U23 X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U52(X1, X2) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# U16 X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U52(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U52(X1, X2) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U52(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U52(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U52(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U52(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U52(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U52(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U52(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U62(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U62(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U62(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U62(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U62(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U62(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U62(X1, X2, X3) -> mark# X1, mark# U41 X -> mark# X) (mark# U62(X1, X2, X3) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U62(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U62(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U62(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U62(X1, X2, X3) -> mark# X1, mark# U23 X -> mark# X) (mark# U62(X1, X2, X3) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U62(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U62(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U62(X1, X2, X3) -> mark# X1, mark# U16 X -> mark# X) (mark# U62(X1, X2, X3) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U62(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U62(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U62(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U62(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U62(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U62(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U62(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U62(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U62(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U62(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U62(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U64(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U64(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U64(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U64(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U64(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U64(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U64(X1, X2, X3) -> mark# X1, mark# U41 X -> mark# X) (mark# U64(X1, X2, X3) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U64(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U64(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U64(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U64(X1, X2, X3) -> mark# X1, mark# U23 X -> mark# X) (mark# U64(X1, X2, X3) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U64(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U64(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U64(X1, X2, X3) -> mark# X1, mark# U16 X -> mark# X) (mark# U64(X1, X2, X3) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U64(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U64(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U64(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U64(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U64(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U64(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U64(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U64(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U64(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U64(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U64(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (a__isNatKind# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) (a__isNatKind# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__isNatKind# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (a__isNatKind# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U11#(tt(), V1, V2) -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) (a__U11#(tt(), V1, V2) -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U11#(tt(), V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (a__U11#(tt(), V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U14#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNatKind V1, V1, V2)) (a__U14#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__U14#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U14#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__isNat# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) (a__isNat# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__isNat# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (a__isNat# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) (a__U21#(tt(), V1) -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (a__U21#(tt(), V1) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> a__U51#(a__isNat N, N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> a__isNat# N) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__U61#(a__isNat M, M, N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__isNat# M) (a__U62#(tt(), M, N) -> a__U63#(a__isNat N, M, N), a__U63#(tt(), M, N) -> a__U64#(a__isNatKind N, M, N)) (a__U62#(tt(), M, N) -> a__U63#(a__isNat N, M, N), a__U63#(tt(), M, N) -> a__isNatKind# N) (a__U63#(tt(), M, N) -> a__U64#(a__isNatKind N, M, N), a__U64#(tt(), M, N) -> a__plus#(mark N, mark M)) (a__U63#(tt(), M, N) -> a__U64#(a__isNatKind N, M, N), a__U64#(tt(), M, N) -> mark# M) (a__U63#(tt(), M, N) -> a__U64#(a__isNatKind N, M, N), a__U64#(tt(), M, N) -> mark# N) (mark# U15(X1, X2) -> a__U15#(mark X1, X2), a__U15#(tt(), V2) -> a__U16# a__isNat V2) (mark# U15(X1, X2) -> a__U15#(mark X1, X2), a__U15#(tt(), V2) -> a__isNat# V2) (mark# U22(X1, X2) -> a__U22#(mark X1, X2), a__U22#(tt(), V1) -> a__U23# a__isNat V1) (mark# U22(X1, X2) -> a__U22#(mark X1, X2), a__U22#(tt(), V1) -> a__isNat# V1) (mark# U51(X1, X2) -> a__U51#(mark X1, X2), a__U51#(tt(), N) -> a__U52#(a__isNatKind N, N)) (mark# U51(X1, X2) -> a__U51#(mark X1, X2), a__U51#(tt(), N) -> a__isNatKind# N) (a__U12#(tt(), V1, V2) -> a__isNatKind# V2, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) (a__U12#(tt(), V1, V2) -> a__isNatKind# V2, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U12#(tt(), V1, V2) -> a__isNatKind# V2, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (a__U12#(tt(), V1, V2) -> a__isNatKind# V2, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U15#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__U11#(a__isNatKind V1, V1, V2)) (a__U15#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__U15#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U15#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__U22#(a__isNatKind V1, V1), a__U22#(tt(), V1) -> a__U23# a__isNat V1) (a__U21#(tt(), V1) -> a__U22#(a__isNatKind V1, V1), a__U22#(tt(), V1) -> a__isNat# V1) (a__U12#(tt(), V1, V2) -> a__U13#(a__isNatKind V2, V1, V2), a__U13#(tt(), V1, V2) -> a__U14#(a__isNatKind V2, V1, V2)) (a__U12#(tt(), V1, V2) -> a__U13#(a__isNatKind V2, V1, V2), a__U13#(tt(), V1, V2) -> a__isNatKind# V2) (a__U13#(tt(), V1, V2) -> a__U14#(a__isNatKind V2, V1, V2), a__U14#(tt(), V1, V2) -> a__isNat# V1) (a__U13#(tt(), V1, V2) -> a__U14#(a__isNatKind V2, V1, V2), a__U14#(tt(), V1, V2) -> a__U15#(a__isNat V1, V2)) (a__U52#(tt(), N) -> mark# N, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (a__U52#(tt(), N) -> mark# N, mark# U64(X1, X2, X3) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (a__U52#(tt(), N) -> mark# N, mark# U63(X1, X2, X3) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (a__U52#(tt(), N) -> mark# N, mark# U62(X1, X2, X3) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (a__U52#(tt(), N) -> mark# N, mark# U61(X1, X2, X3) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U52(X1, X2) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (a__U52#(tt(), N) -> mark# N, mark# U51(X1, X2) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (a__U52#(tt(), N) -> mark# N, mark# U41 X -> mark# X) (a__U52#(tt(), N) -> mark# N, mark# U41 X -> a__U41# mark X) (a__U52#(tt(), N) -> mark# N, mark# U32 X -> mark# X) (a__U52#(tt(), N) -> mark# N, mark# U32 X -> a__U32# mark X) (a__U52#(tt(), N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U52#(tt(), N) -> mark# N, mark# U23 X -> mark# X) (a__U52#(tt(), N) -> mark# N, mark# U23 X -> a__U23# mark X) (a__U52#(tt(), N) -> mark# N, mark# U22(X1, X2) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (a__U52#(tt(), N) -> mark# N, mark# U21(X1, X2) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U52#(tt(), N) -> mark# N, mark# U16 X -> mark# X) (a__U52#(tt(), N) -> mark# N, mark# U16 X -> a__U16# mark X) (a__U52#(tt(), N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U52#(tt(), N) -> mark# N, mark# U15(X1, X2) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (a__U52#(tt(), N) -> mark# N, mark# U14(X1, X2, X3) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (a__U52#(tt(), N) -> mark# N, mark# U13(X1, X2, X3) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (a__U52#(tt(), N) -> mark# N, mark# isNatKind X -> a__isNatKind# X) (a__U52#(tt(), N) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U52#(tt(), N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U52#(tt(), N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U52#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U52#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U52#(tt(), N) -> mark# N, mark# s X -> mark# X) (a__U62#(tt(), M, N) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__isNatKind V1, V1, V2)) (a__U62#(tt(), M, N) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__U62#(tt(), M, N) -> a__isNat# N, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U62#(tt(), M, N) -> a__isNat# N, a__isNat# s V1 -> a__isNatKind# V1) (a__U64#(tt(), M, N) -> mark# N, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# N, mark# U64(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# N, mark# U63(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# N, mark# U62(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# N, mark# U61(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U52(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (a__U64#(tt(), M, N) -> mark# N, mark# U51(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (a__U64#(tt(), M, N) -> mark# N, mark# U41 X -> mark# X) (a__U64#(tt(), M, N) -> mark# N, mark# U41 X -> a__U41# mark X) (a__U64#(tt(), M, N) -> mark# N, mark# U32 X -> mark# X) (a__U64#(tt(), M, N) -> mark# N, mark# U32 X -> a__U32# mark X) (a__U64#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U64#(tt(), M, N) -> mark# N, mark# U23 X -> mark# X) (a__U64#(tt(), M, N) -> mark# N, mark# U23 X -> a__U23# mark X) (a__U64#(tt(), M, N) -> mark# N, mark# U22(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (a__U64#(tt(), M, N) -> mark# N, mark# U21(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U64#(tt(), M, N) -> mark# N, mark# U16 X -> mark# X) (a__U64#(tt(), M, N) -> mark# N, mark# U16 X -> a__U16# mark X) (a__U64#(tt(), M, N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U64#(tt(), M, N) -> mark# N, mark# U15(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (a__U64#(tt(), M, N) -> mark# N, mark# U14(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# N, mark# U13(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# N, mark# isNatKind X -> a__isNatKind# X) (a__U64#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U64#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U64#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U64#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U64#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (mark# s X -> mark# X, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U64(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U63(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U62(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# s X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# s X -> mark# X, mark# U41 X -> mark# X) (mark# s X -> mark# X, mark# U41 X -> a__U41# mark X) (mark# s X -> mark# X, mark# U32 X -> mark# X) (mark# s X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# s X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# s X -> mark# X, mark# U23 X -> mark# X) (mark# s X -> mark# X, mark# U23 X -> a__U23# mark X) (mark# s X -> mark# X, mark# U22(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# s X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# s X -> mark# X, mark# U16 X -> mark# X) (mark# s X -> mark# X, mark# U16 X -> a__U16# mark X) (mark# s X -> mark# X, mark# isNat X -> a__isNat# X) (mark# s X -> mark# X, mark# U15(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# s X -> mark# X, mark# U14(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U13(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__U11#(a__isNatKind V1, V1, V2)) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__isNatKind# V1) (mark# U23 X -> mark# X, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U23 X -> mark# X, mark# U64(X1, X2, X3) -> mark# X1) (mark# U23 X -> mark# X, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U23 X -> mark# X, mark# U63(X1, X2, X3) -> mark# X1) (mark# U23 X -> mark# X, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U23 X -> mark# X, mark# U62(X1, X2, X3) -> mark# X1) (mark# U23 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U23 X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# U23 X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# U23 X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U23 X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# U23 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U23 X -> mark# X, mark# U41 X -> mark# X) (mark# U23 X -> mark# X, mark# U41 X -> a__U41# mark X) (mark# U23 X -> mark# X, mark# U32 X -> mark# X) (mark# U23 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U23 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U23 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U23 X -> mark# X, mark# U23 X -> mark# X) (mark# U23 X -> mark# X, mark# U23 X -> a__U23# mark X) (mark# U23 X -> mark# X, mark# U22(X1, X2) -> mark# X1) (mark# U23 X -> mark# X, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U23 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U23 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U23 X -> mark# X, mark# U16 X -> mark# X) (mark# U23 X -> mark# X, mark# U16 X -> a__U16# mark X) (mark# U23 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U23 X -> mark# X, mark# U15(X1, X2) -> mark# X1) (mark# U23 X -> mark# X, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U23 X -> mark# X, mark# U14(X1, X2, X3) -> mark# X1) (mark# U23 X -> mark# X, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U23 X -> mark# X, mark# U13(X1, X2, X3) -> mark# X1) (mark# U23 X -> mark# X, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U23 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U23 X -> mark# X, mark# U12(X1, X2, X3) -> mark# X1) (mark# U23 X -> mark# X, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U23 X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# U23 X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U23 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U23 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U23 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U23 X -> mark# X, mark# s X -> mark# X) (mark# U41 X -> mark# X, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U41 X -> mark# X, mark# U64(X1, X2, X3) -> mark# X1) (mark# U41 X -> mark# X, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U41 X -> mark# X, mark# U63(X1, X2, X3) -> mark# X1) (mark# U41 X -> mark# X, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U41 X -> mark# X, mark# U62(X1, X2, X3) -> mark# X1) (mark# U41 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U41 X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# U41 X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# U41 X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U41 X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# U41 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U41 X -> mark# X, mark# U41 X -> mark# X) (mark# U41 X -> mark# X, mark# U41 X -> a__U41# mark X) (mark# U41 X -> mark# X, mark# U32 X -> mark# X) (mark# U41 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U41 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U41 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U41 X -> mark# X, mark# U23 X -> mark# X) (mark# U41 X -> mark# X, mark# U23 X -> a__U23# mark X) (mark# U41 X -> mark# X, mark# U22(X1, X2) -> mark# X1) (mark# U41 X -> mark# X, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U41 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U41 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U41 X -> mark# X, mark# U16 X -> mark# X) (mark# U41 X -> mark# X, mark# U16 X -> a__U16# mark X) (mark# U41 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U41 X -> mark# X, mark# U15(X1, X2) -> mark# X1) (mark# U41 X -> mark# X, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U41 X -> mark# X, mark# U14(X1, X2, X3) -> mark# X1) (mark# U41 X -> mark# X, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U41 X -> mark# X, mark# U13(X1, X2, X3) -> mark# X1) (mark# U41 X -> mark# X, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U41 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U41 X -> mark# X, mark# U12(X1, X2, X3) -> mark# X1) (mark# U41 X -> mark# X, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U41 X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# U41 X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U41 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U41 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U41 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U41 X -> mark# X, mark# s X -> mark# X) (mark# U32 X -> mark# X, mark# s X -> mark# X) (mark# U32 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U32 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U32 X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U12(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U32 X -> mark# X, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U13(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U14(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U15(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U32 X -> mark# X, mark# U16 X -> a__U16# mark X) (mark# U32 X -> mark# X, mark# U16 X -> mark# X) (mark# U32 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U22(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U23 X -> a__U23# mark X) (mark# U32 X -> mark# X, mark# U23 X -> mark# X) (mark# U32 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U32 X -> mark# X, mark# U32 X -> mark# X) (mark# U32 X -> mark# X, mark# U41 X -> a__U41# mark X) (mark# U32 X -> mark# X, mark# U41 X -> mark# X) (mark# U32 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U62(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U63(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U64(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U16 X -> mark# X, mark# s X -> mark# X) (mark# U16 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U16 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U16 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U16 X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U16 X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# U16 X -> mark# X, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U16 X -> mark# X, mark# U12(X1, X2, X3) -> mark# X1) (mark# U16 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U16 X -> mark# X, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U16 X -> mark# X, mark# U13(X1, X2, X3) -> mark# X1) (mark# U16 X -> mark# X, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U16 X -> mark# X, mark# U14(X1, X2, X3) -> mark# X1) (mark# U16 X -> mark# X, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U16 X -> mark# X, mark# U15(X1, X2) -> mark# X1) (mark# U16 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U16 X -> mark# X, mark# U16 X -> a__U16# mark X) (mark# U16 X -> mark# X, mark# U16 X -> mark# X) (mark# U16 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U16 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U16 X -> mark# X, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U16 X -> mark# X, mark# U22(X1, X2) -> mark# X1) (mark# U16 X -> mark# X, mark# U23 X -> a__U23# mark X) (mark# U16 X -> mark# X, mark# U23 X -> mark# X) (mark# U16 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U16 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U16 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U16 X -> mark# X, mark# U32 X -> mark# X) (mark# U16 X -> mark# X, mark# U41 X -> a__U41# mark X) (mark# U16 X -> mark# X, mark# U41 X -> mark# X) (mark# U16 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U16 X -> mark# X, mark# U51(X1, X2) -> mark# X1) (mark# U16 X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U16 X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# U16 X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# U16 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U16 X -> mark# X, mark# U62(X1, X2, X3) -> mark# X1) (mark# U16 X -> mark# X, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U16 X -> mark# X, mark# U63(X1, X2, X3) -> mark# X1) (mark# U16 X -> mark# X, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U16 X -> mark# X, mark# U64(X1, X2, X3) -> mark# X1) (mark# U16 X -> mark# X, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# isNatKind X -> a__isNatKind# X, a__isNatKind# s V1 -> a__isNatKind# V1) (mark# isNatKind X -> a__isNatKind# X, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (mark# isNatKind X -> a__isNatKind# X, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (mark# isNatKind X -> a__isNatKind# X, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__isNatKind# V1) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__isNatKind V1, V1, V2)) (a__U63#(tt(), M, N) -> a__isNatKind# N, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U63#(tt(), M, N) -> a__isNatKind# N, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (a__U63#(tt(), M, N) -> a__isNatKind# N, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U63#(tt(), M, N) -> a__isNatKind# N, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) (a__U51#(tt(), N) -> a__isNatKind# N, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U51#(tt(), N) -> a__isNatKind# N, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (a__U51#(tt(), N) -> a__isNatKind# N, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U51#(tt(), N) -> a__isNatKind# N, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) (a__isNat# plus(V1, V2) -> a__U11#(a__isNatKind V1, V1, V2), a__U11#(tt(), V1, V2) -> a__U12#(a__isNatKind V1, V1, V2)) (a__isNat# plus(V1, V2) -> a__U11#(a__isNatKind V1, V1, V2), a__U11#(tt(), V1, V2) -> a__isNatKind# V1) (a__U11#(tt(), V1, V2) -> a__U12#(a__isNatKind V1, V1, V2), a__U12#(tt(), V1, V2) -> a__isNatKind# V2) (a__U11#(tt(), V1, V2) -> a__U12#(a__isNatKind V1, V1, V2), a__U12#(tt(), V1, V2) -> a__U13#(a__isNatKind V2, V1, V2)) (a__U31#(tt(), V2) -> a__isNatKind# V2, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U31#(tt(), V2) -> a__isNatKind# V2, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (a__U31#(tt(), V2) -> a__isNatKind# V2, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U31#(tt(), V2) -> a__isNatKind# V2, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) (a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__U21#(tt(), V1) -> a__isNatKind# V1) (a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__U21#(tt(), V1) -> a__U22#(a__isNatKind V1, V1)) (a__U13#(tt(), V1, V2) -> a__isNatKind# V2, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U13#(tt(), V1, V2) -> a__isNatKind# V2, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (a__U13#(tt(), V1, V2) -> a__isNatKind# V2, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U13#(tt(), V1, V2) -> a__isNatKind# V2, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) (mark# U52(X1, X2) -> a__U52#(mark X1, X2), a__U52#(tt(), N) -> mark# N) (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), V2) -> a__isNatKind# V2) (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), V2) -> a__U32# a__isNatKind V2) (mark# U21(X1, X2) -> a__U21#(mark X1, X2), a__U21#(tt(), V1) -> a__isNatKind# V1) (mark# U21(X1, X2) -> a__U21#(mark X1, X2), a__U21#(tt(), V1) -> a__U22#(a__isNatKind V1, V1)) (a__plus#(N, s M) -> a__U61#(a__isNat M, M, N), a__U61#(tt(), M, N) -> a__isNatKind# M) (a__plus#(N, s M) -> a__U61#(a__isNat M, M, N), a__U61#(tt(), M, N) -> a__U62#(a__isNatKind M, M, N)) (a__U61#(tt(), M, N) -> a__U62#(a__isNatKind M, M, N), a__U62#(tt(), M, N) -> a__isNat# N) (a__U61#(tt(), M, N) -> a__U62#(a__isNatKind M, M, N), a__U62#(tt(), M, N) -> a__U63#(a__isNat N, M, N)) (a__U64#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__isNat# M) (a__U64#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U61#(a__isNat M, M, N)) (a__U64#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__isNat# N) (a__U64#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__U51#(a__isNat N, N)) (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# isNatKind X -> a__isNatKind# X) (mark# plus(X1, X2) -> mark# X2, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U13(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U14(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U15(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (mark# plus(X1, X2) -> mark# X2, mark# U16 X -> a__U16# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U16 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U21(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U22(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U23 X -> a__U23# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U23 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U32 X -> a__U32# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U32 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U41 X -> a__U41# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U41 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U51(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U52(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U61(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U62(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U63(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U64(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (a__U22#(tt(), V1) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U22#(tt(), V1) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U22#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__U22#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNatKind V1, V1, V2)) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) (a__U14#(tt(), V1, V2) -> a__U15#(a__isNat V1, V2), a__U15#(tt(), V2) -> a__isNat# V2) (a__U14#(tt(), V1, V2) -> a__U15#(a__isNat V1, V2), a__U15#(tt(), V2) -> a__U16# a__isNat V2) (a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2), a__U31#(tt(), V2) -> a__isNatKind# V2) (a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2), a__U31#(tt(), V2) -> a__U32# a__isNatKind V2) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) (mark# U63(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U63(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U63(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U63(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U63(X1, X2, X3) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U63(X1, X2, X3) -> mark# X1, mark# U16 X -> mark# X) (mark# U63(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U63(X1, X2, X3) -> mark# X1, mark# U23 X -> mark# X) (mark# U63(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U63(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U63(X1, X2, X3) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U63(X1, X2, X3) -> mark# X1, mark# U41 X -> mark# X) (mark# U63(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U63(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U63(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U61(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U61(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U16 X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U23 X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U41 X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U51(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U51(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U51(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U51(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U51(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U51(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U51(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U51(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U51(X1, X2) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U51(X1, X2) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U51(X1, X2) -> mark# X1, mark# U16 X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U51(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U51(X1, X2) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U51(X1, X2) -> mark# X1, mark# U23 X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U51(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U51(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U51(X1, X2) -> mark# X1, mark# U41 X -> mark# X) (mark# U51(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U51(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U51(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U51(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U51(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U51(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U22(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U22(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U22(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U22(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U22(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U22(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U22(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U22(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U22(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U22(X1, X2) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U22(X1, X2) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U22(X1, X2) -> mark# X1, mark# U16 X -> mark# X) (mark# U22(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U22(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U22(X1, X2) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U22(X1, X2) -> mark# X1, mark# U23 X -> mark# X) (mark# U22(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U22(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U22(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U22(X1, X2) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U22(X1, X2) -> mark# X1, mark# U41 X -> mark# X) (mark# U22(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U22(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U22(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U22(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U22(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U22(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U15(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U15(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U15(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U15(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U15(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U15(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U15(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U15(X1, X2) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U15(X1, X2) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U15(X1, X2) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U15(X1, X2) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U15(X1, X2) -> mark# X1, mark# U16 X -> mark# X) (mark# U15(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U15(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U15(X1, X2) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U15(X1, X2) -> mark# X1, mark# U23 X -> mark# X) (mark# U15(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U15(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U15(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U15(X1, X2) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U15(X1, X2) -> mark# X1, mark# U41 X -> mark# X) (mark# U15(X1, X2) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U15(X1, X2) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U15(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U15(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U15(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U15(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U15(X1, X2) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U13(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U13(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U13(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U13(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U13(X1, X2, X3) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U13(X1, X2, X3) -> mark# X1, mark# U16 X -> mark# X) (mark# U13(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U13(X1, X2, X3) -> mark# X1, mark# U23 X -> mark# X) (mark# U13(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U13(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U13(X1, X2, X3) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U13(X1, X2, X3) -> mark# X1, mark# U41 X -> mark# X) (mark# U13(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U13(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U13(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> a__U13#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> a__U15#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U16 X -> a__U16# mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U16 X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> a__U22#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U23 X -> a__U23# mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U23 X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U41 X -> a__U41# mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U41 X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> a__U51#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U51(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3)) (a__plus#(N, 0()) -> a__U51#(a__isNat N, N), a__U51#(tt(), N) -> a__isNatKind# N) (a__plus#(N, 0()) -> a__U51#(a__isNat N, N), a__U51#(tt(), N) -> a__U52#(a__isNatKind N, N)) (mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3), a__U64#(tt(), M, N) -> mark# N) (mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3), a__U64#(tt(), M, N) -> mark# M) (mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3), a__U64#(tt(), M, N) -> a__plus#(mark N, mark M)) (mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3), a__U62#(tt(), M, N) -> a__isNat# N) (mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3), a__U62#(tt(), M, N) -> a__U63#(a__isNat N, M, N)) (mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3), a__U14#(tt(), V1, V2) -> a__U15#(a__isNat V1, V2)) (mark# U14(X1, X2, X3) -> a__U14#(mark X1, X2, X3), a__U14#(tt(), V1, V2) -> a__isNat# V1) (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), V1, V2) -> a__isNatKind# V2) (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), V1, V2) -> a__U13#(a__isNatKind V2, V1, V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# s V1 -> a__isNatKind# V1) (a__plus#(N, s M) -> a__isNat# M, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__U11#(a__isNatKind V1, V1, V2)) (a__U61#(tt(), M, N) -> a__isNatKind# M, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U61#(tt(), M, N) -> a__isNatKind# M, a__isNatKind# s V1 -> a__U41# a__isNatKind V1) (a__U61#(tt(), M, N) -> a__isNatKind# M, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U61#(tt(), M, N) -> a__isNatKind# M, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2)) } STATUS: arrows: 0.828673 SCCS (3): Scc: { a__U52#(tt(), N) -> mark# N, a__U51#(tt(), N) -> a__U52#(a__isNatKind N, N), mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> mark# X1, mark# U16 X -> mark# X, mark# U21(X1, X2) -> mark# X1, mark# U22(X1, X2) -> mark# X1, mark# U23 X -> mark# X, mark# U31(X1, X2) -> mark# X1, mark# U32 X -> mark# X, mark# U41 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2), mark# U51(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2), mark# U52(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3), mark# U62(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3), mark# U63(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3), mark# U64(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3), a__U62#(tt(), M, N) -> a__U63#(a__isNat N, M, N), a__U61#(tt(), M, N) -> a__U62#(a__isNatKind M, M, N), a__U63#(tt(), M, N) -> a__U64#(a__isNatKind N, M, N), a__U64#(tt(), M, N) -> mark# N, a__U64#(tt(), M, N) -> mark# M, a__U64#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U61#(a__isNat M, M, N), a__plus#(N, 0()) -> a__U51#(a__isNat N, N)} Scc: { a__U12#(tt(), V1, V2) -> a__U13#(a__isNatKind V2, V1, V2), a__U11#(tt(), V1, V2) -> a__U12#(a__isNatKind V1, V1, V2), a__U13#(tt(), V1, V2) -> a__U14#(a__isNatKind V2, V1, V2), a__U14#(tt(), V1, V2) -> a__U15#(a__isNat V1, V2), a__U14#(tt(), V1, V2) -> a__isNat# V1, a__U15#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__isNat# plus(V1, V2) -> a__U11#(a__isNatKind V1, V1, V2), a__U22#(tt(), V1) -> a__isNat# V1, a__U21#(tt(), V1) -> a__U22#(a__isNatKind V1, V1)} Scc: { a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2), a__U31#(tt(), V2) -> a__isNatKind# V2} SCC (38): Strict: { a__U52#(tt(), N) -> mark# N, a__U51#(tt(), N) -> a__U52#(a__isNatKind N, N), mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1, mark# U13(X1, X2, X3) -> mark# X1, mark# U14(X1, X2, X3) -> mark# X1, mark# U15(X1, X2) -> mark# X1, mark# U16 X -> mark# X, mark# U21(X1, X2) -> mark# X1, mark# U22(X1, X2) -> mark# X1, mark# U23 X -> mark# X, mark# U31(X1, X2) -> mark# X1, mark# U32 X -> mark# X, mark# U41 X -> mark# X, mark# U51(X1, X2) -> a__U51#(mark X1, X2), mark# U51(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2), mark# U52(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3), mark# U62(X1, X2, X3) -> mark# X1, mark# U62(X1, X2, X3) -> a__U62#(mark X1, X2, X3), mark# U63(X1, X2, X3) -> mark# X1, mark# U63(X1, X2, X3) -> a__U63#(mark X1, X2, X3), mark# U64(X1, X2, X3) -> mark# X1, mark# U64(X1, X2, X3) -> a__U64#(mark X1, X2, X3), a__U62#(tt(), M, N) -> a__U63#(a__isNat N, M, N), a__U61#(tt(), M, N) -> a__U62#(a__isNatKind M, M, N), a__U63#(tt(), M, N) -> a__U64#(a__isNatKind N, M, N), a__U64#(tt(), M, N) -> mark# N, a__U64#(tt(), M, N) -> mark# M, a__U64#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U61#(a__isNat M, M, N), a__plus#(N, 0()) -> a__U51#(a__isNat N, N)} Weak: { a__U12(X1, X2, X3) -> U12(X1, X2, X3), a__U12(tt(), V1, V2) -> a__U13(a__isNatKind V2, V1, V2), a__isNatKind X -> isNatKind X, a__isNatKind s V1 -> a__U41 a__isNatKind V1, a__isNatKind 0() -> tt(), a__isNatKind plus(V1, V2) -> a__U31(a__isNatKind V1, V2), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), V1, V2) -> a__U12(a__isNatKind V1, V1, V2), a__U13(X1, X2, X3) -> U13(X1, X2, X3), a__U13(tt(), V1, V2) -> a__U14(a__isNatKind V2, V1, V2), a__U14(X1, X2, X3) -> U14(X1, X2, X3), a__U14(tt(), V1, V2) -> a__U15(a__isNat V1, V2), a__U15(X1, X2) -> U15(X1, X2), a__U15(tt(), V2) -> a__U16 a__isNat V2, a__isNat X -> isNat X, a__isNat s V1 -> a__U21(a__isNatKind V1, V1), a__isNat 0() -> tt(), a__isNat plus(V1, V2) -> a__U11(a__isNatKind V1, V1, V2), a__U16 X -> U16 X, a__U16 tt() -> tt(), a__U22(X1, X2) -> U22(X1, X2), a__U22(tt(), V1) -> a__U23 a__isNat V1, a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22(a__isNatKind V1, V1), a__U23 X -> U23 X, a__U23 tt() -> tt(), a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V2) -> a__U32 a__isNatKind V2, a__U41 X -> U41 X, a__U41 tt() -> tt(), a__U52(X1, X2) -> U52(X1, X2), a__U52(tt(), N) -> mark N, a__U51(X1, X2) -> U51(X1, X2), a__U51(tt(), N) -> a__U52(a__isNatKind N, N), mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3), mark U12(X1, X2, X3) -> a__U12(mark X1, X2, X3), mark isNatKind X -> a__isNatKind X, mark U13(X1, X2, X3) -> a__U13(mark X1, X2, X3), mark U14(X1, X2, X3) -> a__U14(mark X1, X2, X3), mark U15(X1, X2) -> a__U15(mark X1, X2), mark isNat X -> a__isNat X, mark U16 X -> a__U16 mark X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22(X1, X2) -> a__U22(mark X1, X2), mark U23 X -> a__U23 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41 X -> a__U41 mark X, mark U51(X1, X2) -> a__U51(mark X1, X2), mark U52(X1, X2) -> a__U52(mark X1, X2), mark U61(X1, X2, X3) -> a__U61(mark X1, X2, X3), mark U62(X1, X2, X3) -> a__U62(mark X1, X2, X3), mark U63(X1, X2, X3) -> a__U63(mark X1, X2, X3), mark U64(X1, X2, X3) -> a__U64(mark X1, X2, X3), a__U62(X1, X2, X3) -> U62(X1, X2, X3), a__U62(tt(), M, N) -> a__U63(a__isNat N, M, N), a__U61(X1, X2, X3) -> U61(X1, X2, X3), a__U61(tt(), M, N) -> a__U62(a__isNatKind M, M, N), a__U63(X1, X2, X3) -> U63(X1, X2, X3), a__U63(tt(), M, N) -> a__U64(a__isNatKind N, M, N), a__U64(X1, X2, X3) -> U64(X1, X2, X3), a__U64(tt(), M, N) -> s a__plus(mark N, mark M), a__plus(N, s M) -> a__U61(a__isNat M, M, N), a__plus(N, 0()) -> a__U51(a__isNat N, N), a__plus(X1, X2) -> plus(X1, X2)} Open SCC (10): Strict: { a__U12#(tt(), V1, V2) -> a__U13#(a__isNatKind V2, V1, V2), a__U11#(tt(), V1, V2) -> a__U12#(a__isNatKind V1, V1, V2), a__U13#(tt(), V1, V2) -> a__U14#(a__isNatKind V2, V1, V2), a__U14#(tt(), V1, V2) -> a__U15#(a__isNat V1, V2), a__U14#(tt(), V1, V2) -> a__isNat# V1, a__U15#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__isNat# plus(V1, V2) -> a__U11#(a__isNatKind V1, V1, V2), a__U22#(tt(), V1) -> a__isNat# V1, a__U21#(tt(), V1) -> a__U22#(a__isNatKind V1, V1)} Weak: { a__U12(X1, X2, X3) -> U12(X1, X2, X3), a__U12(tt(), V1, V2) -> a__U13(a__isNatKind V2, V1, V2), a__isNatKind X -> isNatKind X, a__isNatKind s V1 -> a__U41 a__isNatKind V1, a__isNatKind 0() -> tt(), a__isNatKind plus(V1, V2) -> a__U31(a__isNatKind V1, V2), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), V1, V2) -> a__U12(a__isNatKind V1, V1, V2), a__U13(X1, X2, X3) -> U13(X1, X2, X3), a__U13(tt(), V1, V2) -> a__U14(a__isNatKind V2, V1, V2), a__U14(X1, X2, X3) -> U14(X1, X2, X3), a__U14(tt(), V1, V2) -> a__U15(a__isNat V1, V2), a__U15(X1, X2) -> U15(X1, X2), a__U15(tt(), V2) -> a__U16 a__isNat V2, a__isNat X -> isNat X, a__isNat s V1 -> a__U21(a__isNatKind V1, V1), a__isNat 0() -> tt(), a__isNat plus(V1, V2) -> a__U11(a__isNatKind V1, V1, V2), a__U16 X -> U16 X, a__U16 tt() -> tt(), a__U22(X1, X2) -> U22(X1, X2), a__U22(tt(), V1) -> a__U23 a__isNat V1, a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22(a__isNatKind V1, V1), a__U23 X -> U23 X, a__U23 tt() -> tt(), a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V2) -> a__U32 a__isNatKind V2, a__U41 X -> U41 X, a__U41 tt() -> tt(), a__U52(X1, X2) -> U52(X1, X2), a__U52(tt(), N) -> mark N, a__U51(X1, X2) -> U51(X1, X2), a__U51(tt(), N) -> a__U52(a__isNatKind N, N), mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3), mark U12(X1, X2, X3) -> a__U12(mark X1, X2, X3), mark isNatKind X -> a__isNatKind X, mark U13(X1, X2, X3) -> a__U13(mark X1, X2, X3), mark U14(X1, X2, X3) -> a__U14(mark X1, X2, X3), mark U15(X1, X2) -> a__U15(mark X1, X2), mark isNat X -> a__isNat X, mark U16 X -> a__U16 mark X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22(X1, X2) -> a__U22(mark X1, X2), mark U23 X -> a__U23 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41 X -> a__U41 mark X, mark U51(X1, X2) -> a__U51(mark X1, X2), mark U52(X1, X2) -> a__U52(mark X1, X2), mark U61(X1, X2, X3) -> a__U61(mark X1, X2, X3), mark U62(X1, X2, X3) -> a__U62(mark X1, X2, X3), mark U63(X1, X2, X3) -> a__U63(mark X1, X2, X3), mark U64(X1, X2, X3) -> a__U64(mark X1, X2, X3), a__U62(X1, X2, X3) -> U62(X1, X2, X3), a__U62(tt(), M, N) -> a__U63(a__isNat N, M, N), a__U61(X1, X2, X3) -> U61(X1, X2, X3), a__U61(tt(), M, N) -> a__U62(a__isNatKind M, M, N), a__U63(X1, X2, X3) -> U63(X1, X2, X3), a__U63(tt(), M, N) -> a__U64(a__isNatKind N, M, N), a__U64(X1, X2, X3) -> U64(X1, X2, X3), a__U64(tt(), M, N) -> s a__plus(mark N, mark M), a__plus(N, s M) -> a__U61(a__isNat M, M, N), a__plus(N, 0()) -> a__U51(a__isNat N, N), a__plus(X1, X2) -> plus(X1, X2)} Open SCC (4): Strict: { a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__U31#(a__isNatKind V1, V2), a__U31#(tt(), V2) -> a__isNatKind# V2} Weak: { a__U12(X1, X2, X3) -> U12(X1, X2, X3), a__U12(tt(), V1, V2) -> a__U13(a__isNatKind V2, V1, V2), a__isNatKind X -> isNatKind X, a__isNatKind s V1 -> a__U41 a__isNatKind V1, a__isNatKind 0() -> tt(), a__isNatKind plus(V1, V2) -> a__U31(a__isNatKind V1, V2), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), V1, V2) -> a__U12(a__isNatKind V1, V1, V2), a__U13(X1, X2, X3) -> U13(X1, X2, X3), a__U13(tt(), V1, V2) -> a__U14(a__isNatKind V2, V1, V2), a__U14(X1, X2, X3) -> U14(X1, X2, X3), a__U14(tt(), V1, V2) -> a__U15(a__isNat V1, V2), a__U15(X1, X2) -> U15(X1, X2), a__U15(tt(), V2) -> a__U16 a__isNat V2, a__isNat X -> isNat X, a__isNat s V1 -> a__U21(a__isNatKind V1, V1), a__isNat 0() -> tt(), a__isNat plus(V1, V2) -> a__U11(a__isNatKind V1, V1, V2), a__U16 X -> U16 X, a__U16 tt() -> tt(), a__U22(X1, X2) -> U22(X1, X2), a__U22(tt(), V1) -> a__U23 a__isNat V1, a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22(a__isNatKind V1, V1), a__U23 X -> U23 X, a__U23 tt() -> tt(), a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V2) -> a__U32 a__isNatKind V2, a__U41 X -> U41 X, a__U41 tt() -> tt(), a__U52(X1, X2) -> U52(X1, X2), a__U52(tt(), N) -> mark N, a__U51(X1, X2) -> U51(X1, X2), a__U51(tt(), N) -> a__U52(a__isNatKind N, N), mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3), mark U12(X1, X2, X3) -> a__U12(mark X1, X2, X3), mark isNatKind X -> a__isNatKind X, mark U13(X1, X2, X3) -> a__U13(mark X1, X2, X3), mark U14(X1, X2, X3) -> a__U14(mark X1, X2, X3), mark U15(X1, X2) -> a__U15(mark X1, X2), mark isNat X -> a__isNat X, mark U16 X -> a__U16 mark X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22(X1, X2) -> a__U22(mark X1, X2), mark U23 X -> a__U23 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41 X -> a__U41 mark X, mark U51(X1, X2) -> a__U51(mark X1, X2), mark U52(X1, X2) -> a__U52(mark X1, X2), mark U61(X1, X2, X3) -> a__U61(mark X1, X2, X3), mark U62(X1, X2, X3) -> a__U62(mark X1, X2, X3), mark U63(X1, X2, X3) -> a__U63(mark X1, X2, X3), mark U64(X1, X2, X3) -> a__U64(mark X1, X2, X3), a__U62(X1, X2, X3) -> U62(X1, X2, X3), a__U62(tt(), M, N) -> a__U63(a__isNat N, M, N), a__U61(X1, X2, X3) -> U61(X1, X2, X3), a__U61(tt(), M, N) -> a__U62(a__isNatKind M, M, N), a__U63(X1, X2, X3) -> U63(X1, X2, X3), a__U63(tt(), M, N) -> a__U64(a__isNatKind N, M, N), a__U64(X1, X2, X3) -> U64(X1, X2, X3), a__U64(tt(), M, N) -> s a__plus(mark N, mark M), a__plus(N, s M) -> a__U61(a__isNat M, M, N), a__plus(N, 0()) -> a__U51(a__isNat N, N), a__plus(X1, X2) -> plus(X1, X2)} Open