MAYBE Time: 0.132220 TRS: { a__U12(X1, X2) -> U12(X1, X2), a__U12(tt(), V2) -> a__U13 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__and(a__isNatKind V1, isNatKind V2), V1, V2), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), V1, V2) -> a__U12(a__isNat V1, V2), a__U13 X -> U13 X, a__U13 tt() -> tt(), a__U22 X -> U22 X, a__U22 tt() -> tt(), a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22 a__isNat V1, mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark isNatKind X -> a__isNatKind X, mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark and(X1, X2) -> a__and(mark X1, X2), mark isNat X -> a__isNat X, mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3), mark U12(X1, X2) -> a__U12(mark X1, X2), mark U13 X -> a__U13 mark X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22 X -> a__U22 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U41(X1, X2, X3) -> a__U41(mark X1, X2, X3), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), N) -> mark N, a__plus(N, s M) -> a__U41(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__plus(N, 0()) -> a__U31(a__and(a__isNat N, isNatKind N), N), a__plus(X1, X2) -> plus(X1, X2), a__U41(X1, X2, X3) -> U41(X1, X2, X3), a__U41(tt(), M, N) -> s a__plus(mark N, mark M), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__isNatKind X -> isNatKind X, a__isNatKind s V1 -> a__isNatKind V1, a__isNatKind 0() -> tt(), a__isNatKind plus(V1, V2) -> a__and(a__isNatKind V1, isNatKind V2)} DP: DP: { a__U12#(tt(), V2) -> a__isNat# V2, a__U12#(tt(), V2) -> a__U13# a__isNat V2, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__isNat# s V1 -> a__isNatKind# V1, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2), a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__isNat# plus(V1, V2) -> a__isNatKind# V1, a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2), a__U11#(tt(), V1, V2) -> a__isNat# V1, a__U21#(tt(), V1) -> a__isNat# V1, a__U21#(tt(), V1) -> a__U22# a__isNat V1, mark# s X -> mark# X, mark# isNatKind X -> a__isNatKind# X, mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), mark# isNat X -> a__isNat# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2), mark# U12(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X, mark# U13 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2), mark# U21(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X, mark# U22 X -> mark# X, mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2), mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U31#(tt(), N) -> mark# N, a__plus#(N, s M) -> a__isNat# M, a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M), a__plus#(N, s M) -> a__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), a__plus#(N, 0()) -> a__isNat# N, a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind N), N), a__plus#(N, 0()) -> a__and#(a__isNat N, isNatKind N), a__U41#(tt(), M, N) -> mark# N, a__U41#(tt(), M, N) -> mark# M, a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__and#(tt(), X) -> mark# X, a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__isNatKind# plus(V1, V2) -> a__isNatKind# V1} TRS: { a__U12(X1, X2) -> U12(X1, X2), a__U12(tt(), V2) -> a__U13 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__and(a__isNatKind V1, isNatKind V2), V1, V2), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), V1, V2) -> a__U12(a__isNat V1, V2), a__U13 X -> U13 X, a__U13 tt() -> tt(), a__U22 X -> U22 X, a__U22 tt() -> tt(), a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22 a__isNat V1, mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark isNatKind X -> a__isNatKind X, mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark and(X1, X2) -> a__and(mark X1, X2), mark isNat X -> a__isNat X, mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3), mark U12(X1, X2) -> a__U12(mark X1, X2), mark U13 X -> a__U13 mark X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22 X -> a__U22 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U41(X1, X2, X3) -> a__U41(mark X1, X2, X3), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), N) -> mark N, a__plus(N, s M) -> a__U41(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__plus(N, 0()) -> a__U31(a__and(a__isNat N, isNatKind N), N), a__plus(X1, X2) -> plus(X1, X2), a__U41(X1, X2, X3) -> U41(X1, X2, X3), a__U41(tt(), M, N) -> s a__plus(mark N, mark M), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__isNatKind X -> isNatKind X, a__isNatKind s V1 -> a__isNatKind V1, a__isNatKind 0() -> tt(), a__isNatKind plus(V1, V2) -> a__and(a__isNatKind V1, isNatKind V2)} UR: { a__U12(X1, X2) -> U12(X1, X2), a__U12(tt(), V2) -> a__U13 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__and(a__isNatKind V1, isNatKind V2), V1, V2), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), V1, V2) -> a__U12(a__isNat V1, V2), a__U13 X -> U13 X, a__U13 tt() -> tt(), a__U22 X -> U22 X, a__U22 tt() -> tt(), a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22 a__isNat V1, mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark isNatKind X -> a__isNatKind X, mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark and(X1, X2) -> a__and(mark X1, X2), mark isNat X -> a__isNat X, mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3), mark U12(X1, X2) -> a__U12(mark X1, X2), mark U13 X -> a__U13 mark X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22 X -> a__U22 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U41(X1, X2, X3) -> a__U41(mark X1, X2, X3), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), N) -> mark N, a__plus(N, s M) -> a__U41(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__plus(N, 0()) -> a__U31(a__and(a__isNat N, isNatKind N), N), a__plus(X1, X2) -> plus(X1, X2), a__U41(X1, X2, X3) -> U41(X1, X2, X3), a__U41(tt(), M, N) -> s a__plus(mark N, mark M), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__isNatKind X -> isNatKind X, a__isNatKind s V1 -> a__isNatKind V1, a__isNatKind 0() -> tt(), a__isNatKind plus(V1, V2) -> a__and(a__isNatKind V1, isNatKind V2), a(x, y) -> x, a(x, y) -> y} EDG: { (a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2), a__U12#(tt(), V2) -> a__U13# a__isNat V2) (a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2), a__U12#(tt(), V2) -> a__isNat# V2) (a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__U41#(tt(), M, N) -> a__plus#(mark N, mark M)) (a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__U41#(tt(), M, N) -> mark# M) (a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__U41#(tt(), M, N) -> mark# N) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> a__plus#(mark N, mark M)) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> mark# M) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> mark# N) (mark# U12(X1, X2) -> a__U12#(mark X1, X2), a__U12#(tt(), V2) -> a__U13# a__isNat V2) (mark# U12(X1, X2) -> a__U12#(mark X1, X2), a__U12#(tt(), V2) -> a__isNat# V2) (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), N) -> mark# N) (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__and#(a__isNatKind V1, isNatKind V2)) (mark# isNatKind X -> a__isNatKind# X, a__isNatKind# s V1 -> a__isNatKind# V1) (mark# U13 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U13 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U13 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U13 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# U22 X -> mark# X) (mark# U13 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U13 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U13 X -> mark# X, mark# U13 X -> mark# X) (mark# U13 X -> mark# X, mark# U13 X -> a__U13# mark X) (mark# U13 X -> mark# X, mark# U12(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U13 X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# U13 X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U13 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U13 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U13 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U13 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U13 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U13 X -> mark# X, mark# s X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__and#(tt(), X) -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U31(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U22 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U22 X -> a__U22# mark X) (a__and#(tt(), X) -> mark# X, mark# U21(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U13 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U13 X -> a__U13# mark X) (a__and#(tt(), X) -> mark# X, mark# U12(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__and#(tt(), X) -> mark# X, mark# isNat X -> a__isNat# X) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X2) (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# isNatKind X -> a__isNatKind# X) (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X) (a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2), a__U11#(tt(), V1, V2) -> a__isNat# V1) (a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2)) (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__and#(a__isNatKind V1, isNatKind V2)) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), 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, s M) -> a__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), a__and#(tt(), X) -> mark# X) (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# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNat# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (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# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNatKind# plus(V1, V2) -> 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__and#(a__isNat N, isNatKind N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind 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__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N))) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__isNat# M) (a__plus#(N, 0()) -> a__and#(a__isNat N, isNatKind N), a__and#(tt(), X) -> mark# X) (a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__and#(tt(), X) -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# and(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U12(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U12(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U12(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U12(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# U12(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U12(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U12(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U12(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U12(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U12(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U12(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (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# U13 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (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# isNat X -> a__isNat# X) (mark# U31(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (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# isNatKind X -> a__isNatKind# X) (mark# U31(X1, X2) -> mark# X1, mark# s X -> mark# X) (a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__U21#(tt(), V1) -> a__U22# a__isNat V1) (a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__U21#(tt(), V1) -> a__isNat# V1) (a__U41#(tt(), M, N) -> mark# M, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> mark# M, mark# U41(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U22 X -> mark# X) (a__U41#(tt(), M, N) -> mark# M, mark# U22 X -> a__U22# mark X) (a__U41#(tt(), M, N) -> mark# M, mark# U21(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# U13 X -> mark# X) (a__U41#(tt(), M, N) -> mark# M, mark# U13 X -> a__U13# mark X) (a__U41#(tt(), M, N) -> mark# M, mark# U12(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> mark# M, mark# isNat X -> a__isNat# X) (a__U41#(tt(), M, N) -> mark# M, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# and(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U41#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U41#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# isNatKind X -> a__isNatKind# X) (a__U41#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (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# s V1 -> a__isNatKind# V1) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (mark# U41(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U13 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U22 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U21(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U21(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U22 X -> 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# U41(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# 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# and(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (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) -> a__U12#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U13 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 X -> a__U22# mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22 X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U22 X -> 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# U41(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__isNat# M) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N))) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__isNat# N) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind N), N)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__and#(a__isNat N, isNatKind N)) (a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M), a__and#(tt(), X) -> mark# X) (a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__and#(tt(), X) -> mark# X) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U41#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__U41#(tt(), M, N) -> mark# N, mark# isNatKind X -> a__isNatKind# X) (a__U41#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U41#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U41#(tt(), M, N) -> mark# N, mark# and(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U41#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# U12(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U13 X -> a__U13# mark X) (a__U41#(tt(), M, N) -> mark# N, mark# U13 X -> mark# X) (a__U41#(tt(), M, N) -> mark# N, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# U21(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U22 X -> a__U22# mark X) (a__U41#(tt(), M, N) -> mark# N, mark# U22 X -> mark# X) (a__U41#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# U41(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U31#(tt(), N) -> mark# N, mark# s X -> mark# X) (a__U31#(tt(), N) -> mark# N, mark# isNatKind X -> a__isNatKind# X) (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U31#(tt(), N) -> mark# N, mark# and(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U31#(tt(), N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U31#(tt(), N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# U12(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U13 X -> a__U13# mark X) (a__U31#(tt(), N) -> mark# N, mark# U13 X -> mark# X) (a__U31#(tt(), N) -> mark# N, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# U21(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U22 X -> a__U22# mark X) (a__U31#(tt(), N) -> mark# N, mark# U22 X -> mark# X) (a__U31#(tt(), N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# U41(X1, X2, X3) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind N), N), a__U31#(tt(), N) -> mark# N) (mark# U22 X -> mark# X, mark# s X -> mark# X) (mark# U22 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U22 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U22 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U22 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U22 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U22 X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U22 X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# U22 X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U12(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U13 X -> a__U13# mark X) (mark# U22 X -> mark# X, mark# U13 X -> mark# X) (mark# U22 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U22 X -> mark# X, mark# U22 X -> mark# X) (mark# U22 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U22 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (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# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# s X -> mark# X, mark# isNat X -> a__isNat# X) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# s X -> mark# X, mark# U12(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U13 X -> a__U13# mark X) (mark# s X -> mark# X, mark# U13 X -> mark# X) (mark# s X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# s X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# s X -> mark# X, mark# U22 X -> 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# U41(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U21(X1, X2) -> a__U21#(mark X1, X2), a__U21#(tt(), V1) -> a__isNat# V1) (mark# U21(X1, X2) -> a__U21#(mark X1, X2), a__U21#(tt(), V1) -> a__U22# a__isNat V1) (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X) (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2)) (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), V1, V2) -> a__isNat# V1) (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# isNatKind X -> a__isNatKind# 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# and(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (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) -> a__U12#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U13 X -> a__U13# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U13 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 X -> a__U22# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U22 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__isNatKind# V1) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__isNatKind# V1) } EDG: { (a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2), a__U12#(tt(), V2) -> a__U13# a__isNat V2) (a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2), a__U12#(tt(), V2) -> a__isNat# V2) (a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__U41#(tt(), M, N) -> a__plus#(mark N, mark M)) (a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__U41#(tt(), M, N) -> mark# M) (a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__U41#(tt(), M, N) -> mark# N) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> a__plus#(mark N, mark M)) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> mark# M) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> mark# N) (mark# U12(X1, X2) -> a__U12#(mark X1, X2), a__U12#(tt(), V2) -> a__U13# a__isNat V2) (mark# U12(X1, X2) -> a__U12#(mark X1, X2), a__U12#(tt(), V2) -> a__isNat# V2) (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), N) -> mark# N) (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__and#(a__isNatKind V1, isNatKind V2)) (mark# isNatKind X -> a__isNatKind# X, a__isNatKind# s V1 -> a__isNatKind# V1) (mark# U13 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U13 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U13 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U13 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# U22 X -> mark# X) (mark# U13 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U13 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U13 X -> mark# X, mark# U13 X -> mark# X) (mark# U13 X -> mark# X, mark# U13 X -> a__U13# mark X) (mark# U13 X -> mark# X, mark# U12(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U13 X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# U13 X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U13 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U13 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U13 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U13 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U13 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U13 X -> mark# X, mark# s X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__and#(tt(), X) -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U31(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U22 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U22 X -> a__U22# mark X) (a__and#(tt(), X) -> mark# X, mark# U21(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U13 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U13 X -> a__U13# mark X) (a__and#(tt(), X) -> mark# X, mark# U12(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__and#(tt(), X) -> mark# X, mark# isNat X -> a__isNat# X) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X2) (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# isNatKind X -> a__isNatKind# X) (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X) (a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2), a__U11#(tt(), V1, V2) -> a__isNat# V1) (a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2)) (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__and#(a__isNatKind V1, isNatKind V2)) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), 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, s M) -> a__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), a__and#(tt(), X) -> mark# X) (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# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNat# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (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# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNatKind# plus(V1, V2) -> 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__and#(a__isNat N, isNatKind N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind 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__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N))) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__isNat# M) (a__plus#(N, 0()) -> a__and#(a__isNat N, isNatKind N), a__and#(tt(), X) -> mark# X) (a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__and#(tt(), X) -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# and(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U12(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U12(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U12(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U12(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# U12(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U12(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U12(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U12(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U12(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U12(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U12(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (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# U13 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (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# isNat X -> a__isNat# X) (mark# U31(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (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# isNatKind X -> a__isNatKind# X) (mark# U31(X1, X2) -> mark# X1, mark# s X -> mark# X) (a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__U21#(tt(), V1) -> a__U22# a__isNat V1) (a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__U21#(tt(), V1) -> a__isNat# V1) (a__U41#(tt(), M, N) -> mark# M, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> mark# M, mark# U41(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U22 X -> mark# X) (a__U41#(tt(), M, N) -> mark# M, mark# U22 X -> a__U22# mark X) (a__U41#(tt(), M, N) -> mark# M, mark# U21(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# U13 X -> mark# X) (a__U41#(tt(), M, N) -> mark# M, mark# U13 X -> a__U13# mark X) (a__U41#(tt(), M, N) -> mark# M, mark# U12(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> mark# M, mark# isNat X -> a__isNat# X) (a__U41#(tt(), M, N) -> mark# M, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# and(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U41#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U41#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# isNatKind X -> a__isNatKind# X) (a__U41#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (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# s V1 -> a__isNatKind# V1) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (mark# U41(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U13 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U22 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U21(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U21(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U22 X -> 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# U41(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# 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# and(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (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) -> a__U12#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U13 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 X -> a__U22# mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22 X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U22 X -> 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# U41(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__isNat# M) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N))) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__isNat# N) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind N), N)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__and#(a__isNat N, isNatKind N)) (a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M), a__and#(tt(), X) -> mark# X) (a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__and#(tt(), X) -> mark# X) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U41#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__U41#(tt(), M, N) -> mark# N, mark# isNatKind X -> a__isNatKind# X) (a__U41#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U41#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U41#(tt(), M, N) -> mark# N, mark# and(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U41#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# U12(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U13 X -> a__U13# mark X) (a__U41#(tt(), M, N) -> mark# N, mark# U13 X -> mark# X) (a__U41#(tt(), M, N) -> mark# N, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# U21(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U22 X -> a__U22# mark X) (a__U41#(tt(), M, N) -> mark# N, mark# U22 X -> mark# X) (a__U41#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# U41(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U31#(tt(), N) -> mark# N, mark# s X -> mark# X) (a__U31#(tt(), N) -> mark# N, mark# isNatKind X -> a__isNatKind# X) (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U31#(tt(), N) -> mark# N, mark# and(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U31#(tt(), N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U31#(tt(), N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# U12(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U13 X -> a__U13# mark X) (a__U31#(tt(), N) -> mark# N, mark# U13 X -> mark# X) (a__U31#(tt(), N) -> mark# N, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# U21(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U22 X -> a__U22# mark X) (a__U31#(tt(), N) -> mark# N, mark# U22 X -> mark# X) (a__U31#(tt(), N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# U41(X1, X2, X3) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind N), N), a__U31#(tt(), N) -> mark# N) (mark# U22 X -> mark# X, mark# s X -> mark# X) (mark# U22 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U22 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U22 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U22 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U22 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U22 X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U22 X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# U22 X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U12(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U13 X -> a__U13# mark X) (mark# U22 X -> mark# X, mark# U13 X -> mark# X) (mark# U22 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U22 X -> mark# X, mark# U22 X -> mark# X) (mark# U22 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U22 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (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# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# s X -> mark# X, mark# isNat X -> a__isNat# X) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# s X -> mark# X, mark# U12(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U13 X -> a__U13# mark X) (mark# s X -> mark# X, mark# U13 X -> mark# X) (mark# s X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# s X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# s X -> mark# X, mark# U22 X -> 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# U41(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U21(X1, X2) -> a__U21#(mark X1, X2), a__U21#(tt(), V1) -> a__isNat# V1) (mark# U21(X1, X2) -> a__U21#(mark X1, X2), a__U21#(tt(), V1) -> a__U22# a__isNat V1) (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X) (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2)) (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), V1, V2) -> a__isNat# V1) (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# isNatKind X -> a__isNatKind# 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# and(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (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) -> a__U12#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U13 X -> a__U13# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U13 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 X -> a__U22# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U22 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__isNatKind# V1) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__isNatKind# V1) } EDG: { (a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2), a__U12#(tt(), V2) -> a__U13# a__isNat V2) (a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2), a__U12#(tt(), V2) -> a__isNat# V2) (a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__U41#(tt(), M, N) -> a__plus#(mark N, mark M)) (a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__U41#(tt(), M, N) -> mark# M) (a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__U41#(tt(), M, N) -> mark# N) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> a__plus#(mark N, mark M)) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> mark# M) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> mark# N) (mark# U12(X1, X2) -> a__U12#(mark X1, X2), a__U12#(tt(), V2) -> a__U13# a__isNat V2) (mark# U12(X1, X2) -> a__U12#(mark X1, X2), a__U12#(tt(), V2) -> a__isNat# V2) (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), N) -> mark# N) (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__and#(a__isNatKind V1, isNatKind V2)) (mark# isNatKind X -> a__isNatKind# X, a__isNatKind# s V1 -> a__isNatKind# V1) (mark# U13 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U13 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U13 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U13 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# U22 X -> mark# X) (mark# U13 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U13 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U13 X -> mark# X, mark# U13 X -> mark# X) (mark# U13 X -> mark# X, mark# U13 X -> a__U13# mark X) (mark# U13 X -> mark# X, mark# U12(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U13 X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# U13 X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U13 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U13 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U13 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U13 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U13 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U13 X -> mark# X, mark# s X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__and#(tt(), X) -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U31(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U22 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U22 X -> a__U22# mark X) (a__and#(tt(), X) -> mark# X, mark# U21(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U13 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U13 X -> a__U13# mark X) (a__and#(tt(), X) -> mark# X, mark# U12(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__and#(tt(), X) -> mark# X, mark# isNat X -> a__isNat# X) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X2) (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# isNatKind X -> a__isNatKind# X) (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X) (a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2), a__U11#(tt(), V1, V2) -> a__isNat# V1) (a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2)) (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__and#(a__isNatKind V1, isNatKind V2)) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), 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, s M) -> a__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), a__and#(tt(), X) -> mark# X) (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# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNat# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (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# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNatKind# plus(V1, V2) -> 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__and#(a__isNat N, isNatKind N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind 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__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N))) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__isNat# M) (a__plus#(N, 0()) -> a__and#(a__isNat N, isNatKind N), a__and#(tt(), X) -> mark# X) (a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__and#(tt(), X) -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# and(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U12(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U12(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U12(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U12(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# U12(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U12(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U12(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U12(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U12(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U12(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U12(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (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# U13 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (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# isNat X -> a__isNat# X) (mark# U31(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (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# isNatKind X -> a__isNatKind# X) (mark# U31(X1, X2) -> mark# X1, mark# s X -> mark# X) (a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__U21#(tt(), V1) -> a__U22# a__isNat V1) (a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__U21#(tt(), V1) -> a__isNat# V1) (a__U41#(tt(), M, N) -> mark# M, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> mark# M, mark# U41(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U22 X -> mark# X) (a__U41#(tt(), M, N) -> mark# M, mark# U22 X -> a__U22# mark X) (a__U41#(tt(), M, N) -> mark# M, mark# U21(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# U13 X -> mark# X) (a__U41#(tt(), M, N) -> mark# M, mark# U13 X -> a__U13# mark X) (a__U41#(tt(), M, N) -> mark# M, mark# U12(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> mark# M, mark# isNat X -> a__isNat# X) (a__U41#(tt(), M, N) -> mark# M, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# and(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U41#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U41#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# isNatKind X -> a__isNatKind# X) (a__U41#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (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# s V1 -> a__isNatKind# V1) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (mark# U41(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U13 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U22 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U21(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U21(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U22 X -> 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# U41(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# 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# and(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (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) -> a__U12#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U13 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 X -> a__U22# mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22 X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U22 X -> 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# U41(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__isNat# M) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N))) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__isNat# N) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind N), N)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__and#(a__isNat N, isNatKind N)) (a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M), a__and#(tt(), X) -> mark# X) (a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__and#(tt(), X) -> mark# X) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U41#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__U41#(tt(), M, N) -> mark# N, mark# isNatKind X -> a__isNatKind# X) (a__U41#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U41#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U41#(tt(), M, N) -> mark# N, mark# and(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U41#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# U12(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U13 X -> a__U13# mark X) (a__U41#(tt(), M, N) -> mark# N, mark# U13 X -> mark# X) (a__U41#(tt(), M, N) -> mark# N, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# U21(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U22 X -> a__U22# mark X) (a__U41#(tt(), M, N) -> mark# N, mark# U22 X -> mark# X) (a__U41#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# U41(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U31#(tt(), N) -> mark# N, mark# s X -> mark# X) (a__U31#(tt(), N) -> mark# N, mark# isNatKind X -> a__isNatKind# X) (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U31#(tt(), N) -> mark# N, mark# and(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U31#(tt(), N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U31#(tt(), N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# U12(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U13 X -> a__U13# mark X) (a__U31#(tt(), N) -> mark# N, mark# U13 X -> mark# X) (a__U31#(tt(), N) -> mark# N, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# U21(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U22 X -> a__U22# mark X) (a__U31#(tt(), N) -> mark# N, mark# U22 X -> mark# X) (a__U31#(tt(), N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# U41(X1, X2, X3) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind N), N), a__U31#(tt(), N) -> mark# N) (mark# U22 X -> mark# X, mark# s X -> mark# X) (mark# U22 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U22 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U22 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U22 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U22 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U22 X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U22 X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# U22 X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U12(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U13 X -> a__U13# mark X) (mark# U22 X -> mark# X, mark# U13 X -> mark# X) (mark# U22 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U22 X -> mark# X, mark# U22 X -> mark# X) (mark# U22 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U22 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (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# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# s X -> mark# X, mark# isNat X -> a__isNat# X) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# s X -> mark# X, mark# U12(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U13 X -> a__U13# mark X) (mark# s X -> mark# X, mark# U13 X -> mark# X) (mark# s X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# s X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# s X -> mark# X, mark# U22 X -> 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# U41(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U21(X1, X2) -> a__U21#(mark X1, X2), a__U21#(tt(), V1) -> a__isNat# V1) (mark# U21(X1, X2) -> a__U21#(mark X1, X2), a__U21#(tt(), V1) -> a__U22# a__isNat V1) (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X) (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2)) (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), V1, V2) -> a__isNat# V1) (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# isNatKind X -> a__isNatKind# 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# and(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (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) -> a__U12#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U13 X -> a__U13# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U13 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 X -> a__U22# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U22 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__isNatKind# V1) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__isNatKind# V1) } EDG: { (a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2), a__U12#(tt(), V2) -> a__U13# a__isNat V2) (a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2), a__U12#(tt(), V2) -> a__isNat# V2) (a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__U41#(tt(), M, N) -> a__plus#(mark N, mark M)) (a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__U41#(tt(), M, N) -> mark# M) (a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__U41#(tt(), M, N) -> mark# N) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> a__plus#(mark N, mark M)) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> mark# M) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> mark# N) (mark# U12(X1, X2) -> a__U12#(mark X1, X2), a__U12#(tt(), V2) -> a__U13# a__isNat V2) (mark# U12(X1, X2) -> a__U12#(mark X1, X2), a__U12#(tt(), V2) -> a__isNat# V2) (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), N) -> mark# N) (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__and#(a__isNatKind V1, isNatKind V2)) (mark# isNatKind X -> a__isNatKind# X, a__isNatKind# s V1 -> a__isNatKind# V1) (mark# U13 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U13 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U13 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U13 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# U22 X -> mark# X) (mark# U13 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U13 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U13 X -> mark# X, mark# U13 X -> mark# X) (mark# U13 X -> mark# X, mark# U13 X -> a__U13# mark X) (mark# U13 X -> mark# X, mark# U12(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U13 X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# U13 X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U13 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U13 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U13 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U13 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U13 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U13 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U13 X -> mark# X, mark# s X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__and#(tt(), X) -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U31(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U22 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U22 X -> a__U22# mark X) (a__and#(tt(), X) -> mark# X, mark# U21(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U13 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U13 X -> a__U13# mark X) (a__and#(tt(), X) -> mark# X, mark# U12(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__and#(tt(), X) -> mark# X, mark# isNat X -> a__isNat# X) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X2) (a__and#(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# isNatKind X -> a__isNatKind# X) (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X) (a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2), a__U11#(tt(), V1, V2) -> a__isNat# V1) (a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2)) (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__and#(a__isNatKind V1, isNatKind V2)) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), 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, s M) -> a__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), a__and#(tt(), X) -> mark# X) (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# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNat# plus(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (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# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNatKind# plus(V1, V2) -> 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__and#(a__isNat N, isNatKind N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind 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__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N))) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__isNat# M) (a__plus#(N, 0()) -> a__and#(a__isNat N, isNatKind N), a__and#(tt(), X) -> mark# X) (a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__and#(tt(), X) -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# and(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U12(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U12(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U12(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U12(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# U12(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U12(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U12(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U12(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U12(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U12(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U12(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U12(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U12(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (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# U13 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (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# isNat X -> a__isNat# X) (mark# U31(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (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# isNatKind X -> a__isNatKind# X) (mark# U31(X1, X2) -> mark# X1, mark# s X -> mark# X) (a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__U21#(tt(), V1) -> a__U22# a__isNat V1) (a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__U21#(tt(), V1) -> a__isNat# V1) (a__U41#(tt(), M, N) -> mark# M, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> mark# M, mark# U41(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U22 X -> mark# X) (a__U41#(tt(), M, N) -> mark# M, mark# U22 X -> a__U22# mark X) (a__U41#(tt(), M, N) -> mark# M, mark# U21(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# U13 X -> mark# X) (a__U41#(tt(), M, N) -> mark# M, mark# U13 X -> a__U13# mark X) (a__U41#(tt(), M, N) -> mark# M, mark# U12(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> mark# M, mark# isNat X -> a__isNat# X) (a__U41#(tt(), M, N) -> mark# M, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# M, mark# and(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U41#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U41#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# M, mark# isNatKind X -> a__isNatKind# X) (a__U41#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (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# s V1 -> a__isNatKind# V1) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (mark# U41(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U13 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U22 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U21(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U21(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U21(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U22 X -> 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# U41(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# 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# and(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (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) -> a__U12#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U13 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 X -> a__U22# mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22 X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U13 X -> a__U13# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U13 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U22 X -> 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# U41(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__isNat# M) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N))) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__isNat# N) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind N), N)) (a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__and#(a__isNat N, isNatKind N)) (a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M), a__and#(tt(), X) -> mark# X) (a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__and#(tt(), X) -> mark# X) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__U11#(tt(), V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__isNatKind# V1) (a__U41#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__U41#(tt(), M, N) -> mark# N, mark# isNatKind X -> a__isNatKind# X) (a__U41#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U41#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U41#(tt(), M, N) -> mark# N, mark# and(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U41#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U41#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# U12(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U13 X -> a__U13# mark X) (a__U41#(tt(), M, N) -> mark# N, mark# U13 X -> mark# X) (a__U41#(tt(), M, N) -> mark# N, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# U21(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U22 X -> a__U22# mark X) (a__U41#(tt(), M, N) -> mark# N, mark# U22 X -> mark# X) (a__U41#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U41#(tt(), M, N) -> mark# N, mark# U41(X1, X2, X3) -> mark# X1) (a__U41#(tt(), M, N) -> mark# N, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U31#(tt(), N) -> mark# N, mark# s X -> mark# X) (a__U31#(tt(), N) -> mark# N, mark# isNatKind X -> a__isNatKind# X) (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U31#(tt(), N) -> mark# N, mark# and(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U31#(tt(), N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U31#(tt(), N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# U12(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U13 X -> a__U13# mark X) (a__U31#(tt(), N) -> mark# N, mark# U13 X -> mark# X) (a__U31#(tt(), N) -> mark# N, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# U21(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U22 X -> a__U22# mark X) (a__U31#(tt(), N) -> mark# N, mark# U22 X -> mark# X) (a__U31#(tt(), N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U31#(tt(), N) -> mark# N, mark# U41(X1, X2, X3) -> mark# X1) (a__U31#(tt(), N) -> mark# N, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind N), N), a__U31#(tt(), N) -> mark# N) (mark# U22 X -> mark# X, mark# s X -> mark# X) (mark# U22 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U22 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U22 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U22 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U22 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U22 X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U22 X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# U22 X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U12(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U13 X -> a__U13# mark X) (mark# U22 X -> mark# X, mark# U13 X -> mark# X) (mark# U22 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U22 X -> mark# X, mark# U22 X -> mark# X) (mark# U22 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U22 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (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# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__isNatKind# V1) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# s X -> mark# X, mark# isNat X -> a__isNat# X) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2)) (mark# s X -> mark# X, mark# U12(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U13 X -> a__U13# mark X) (mark# s X -> mark# X, mark# U13 X -> mark# X) (mark# s X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# s X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# s X -> mark# X, mark# U22 X -> 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# U41(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U21(X1, X2) -> a__U21#(mark X1, X2), a__U21#(tt(), V1) -> a__isNat# V1) (mark# U21(X1, X2) -> a__U21#(mark X1, X2), a__U21#(tt(), V1) -> a__U22# a__isNat V1) (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X) (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2)) (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), V1, V2) -> a__isNat# V1) (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# isNatKind X -> a__isNatKind# 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# and(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (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) -> a__U12#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U13 X -> a__U13# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U13 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 X -> a__U22# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U22 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__isNatKind# V1) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2)) (a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__isNatKind# V1) } STATUS: arrows: 0.819878 SCCS (1): Scc: { a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__isNat# s V1 -> a__isNatKind# V1, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2), a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__isNat# plus(V1, V2) -> a__isNatKind# V1, a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2), a__U11#(tt(), V1, V2) -> a__isNat# V1, a__U21#(tt(), V1) -> a__isNat# V1, mark# s X -> mark# X, mark# isNatKind X -> a__isNatKind# X, mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), mark# isNat X -> a__isNat# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2), mark# U12(X1, X2) -> mark# X1, mark# U13 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2), mark# U21(X1, X2) -> mark# X1, mark# U22 X -> mark# X, mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2), mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U31#(tt(), N) -> mark# N, a__plus#(N, s M) -> a__isNat# M, a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M), a__plus#(N, s M) -> a__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), a__plus#(N, 0()) -> a__isNat# N, a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind N), N), a__plus#(N, 0()) -> a__and#(a__isNat N, isNatKind N), a__U41#(tt(), M, N) -> mark# N, a__U41#(tt(), M, N) -> mark# M, a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__and#(tt(), X) -> mark# X, a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__isNatKind# plus(V1, V2) -> a__isNatKind# V1} SCC (44): Strict: { a__U12#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__isNat# s V1 -> a__isNatKind# V1, a__isNat# plus(V1, V2) -> a__U11#(a__and(a__isNatKind V1, isNatKind V2), V1, V2), a__isNat# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__isNat# plus(V1, V2) -> a__isNatKind# V1, a__U11#(tt(), V1, V2) -> a__U12#(a__isNat V1, V2), a__U11#(tt(), V1, V2) -> a__isNat# V1, a__U21#(tt(), V1) -> a__isNat# V1, mark# s X -> mark# X, mark# isNatKind X -> a__isNatKind# X, mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), mark# isNat X -> a__isNat# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2), mark# U12(X1, X2) -> mark# X1, mark# U13 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2), mark# U21(X1, X2) -> mark# X1, mark# U22 X -> mark# X, mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2), mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U31#(tt(), N) -> mark# N, a__plus#(N, s M) -> a__isNat# M, a__plus#(N, s M) -> a__U41#(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__plus#(N, s M) -> a__and#(a__isNat M, isNatKind M), a__plus#(N, s M) -> a__and#(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), a__plus#(N, 0()) -> a__isNat# N, a__plus#(N, 0()) -> a__U31#(a__and(a__isNat N, isNatKind N), N), a__plus#(N, 0()) -> a__and#(a__isNat N, isNatKind N), a__U41#(tt(), M, N) -> mark# N, a__U41#(tt(), M, N) -> mark# M, a__U41#(tt(), M, N) -> a__plus#(mark N, mark M), a__and#(tt(), X) -> mark# X, a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# plus(V1, V2) -> a__and#(a__isNatKind V1, isNatKind V2), a__isNatKind# plus(V1, V2) -> a__isNatKind# V1} Weak: { a__U12(X1, X2) -> U12(X1, X2), a__U12(tt(), V2) -> a__U13 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__and(a__isNatKind V1, isNatKind V2), V1, V2), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), V1, V2) -> a__U12(a__isNat V1, V2), a__U13 X -> U13 X, a__U13 tt() -> tt(), a__U22 X -> U22 X, a__U22 tt() -> tt(), a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22 a__isNat V1, mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark isNatKind X -> a__isNatKind X, mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark and(X1, X2) -> a__and(mark X1, X2), mark isNat X -> a__isNat X, mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3), mark U12(X1, X2) -> a__U12(mark X1, X2), mark U13 X -> a__U13 mark X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22 X -> a__U22 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U41(X1, X2, X3) -> a__U41(mark X1, X2, X3), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), N) -> mark N, a__plus(N, s M) -> a__U41(a__and(a__and(a__isNat M, isNatKind M), and(isNat N, isNatKind N)), M, N), a__plus(N, 0()) -> a__U31(a__and(a__isNat N, isNatKind N), N), a__plus(X1, X2) -> plus(X1, X2), a__U41(X1, X2, X3) -> U41(X1, X2, X3), a__U41(tt(), M, N) -> s a__plus(mark N, mark M), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__isNatKind X -> isNatKind X, a__isNatKind s V1 -> a__isNatKind V1, a__isNatKind 0() -> tt(), a__isNatKind plus(V1, V2) -> a__and(a__isNatKind V1, isNatKind V2)} Open