MAYBE Time: 1.216467 TRS: { a__U12 X -> U12 X, a__U12 tt() -> tt(), a__isNat X -> isNat X, a__isNat s V1 -> a__U21 a__isNat V1, a__isNat 0() -> tt(), a__isNat plus(V1, V2) -> a__U11(a__isNat V1, V2), a__isNat x(V1, V2) -> a__U31(a__isNat V1, V2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), V2) -> a__U12 a__isNat V2, a__U21 X -> U21 X, a__U21 tt() -> tt(), a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V2) -> a__U32 a__isNat V2, mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark x(X1, X2) -> a__x(mark X1, mark X2), mark U11(X1, X2) -> a__U11(mark X1, X2), mark U12 X -> a__U12 mark X, mark isNat X -> a__isNat X, mark U21 X -> a__U21 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41(X1, X2) -> a__U41(mark X1, X2), mark U51(X1, X2, X3) -> a__U51(mark X1, X2, X3), mark U52(X1, X2, X3) -> a__U52(mark X1, X2, X3), mark U61 X -> a__U61 mark X, mark U71(X1, X2, X3) -> a__U71(mark X1, X2, X3), mark U72(X1, X2, X3) -> a__U72(mark X1, X2, X3), a__U41(X1, X2) -> U41(X1, X2), a__U41(tt(), N) -> mark N, a__U52(X1, X2, X3) -> U52(X1, X2, X3), a__U52(tt(), M, N) -> s a__plus(mark N, mark M), a__U51(X1, X2, X3) -> U51(X1, X2, X3), a__U51(tt(), M, N) -> a__U52(a__isNat N, M, N), a__plus(N, s M) -> a__U51(a__isNat M, M, N), a__plus(N, 0()) -> a__U41(a__isNat N, N), a__plus(X1, X2) -> plus(X1, X2), a__U61 X -> U61 X, a__U61 tt() -> 0(), a__U72(X1, X2, X3) -> U72(X1, X2, X3), a__U72(tt(), M, N) -> a__plus(a__x(mark N, mark M), mark N), a__U71(X1, X2, X3) -> U71(X1, X2, X3), a__U71(tt(), M, N) -> a__U72(a__isNat N, M, N), a__x(N, s M) -> a__U71(a__isNat M, M, N), a__x(N, 0()) -> a__U61 a__isNat N, a__x(X1, X2) -> x(X1, X2)} DP: DP: { a__isNat# s V1 -> a__isNat# V1, a__isNat# s V1 -> a__U21# a__isNat V1, a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2), a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2), a__U11#(tt(), V2) -> a__U12# a__isNat V2, a__U11#(tt(), V2) -> a__isNat# V2, a__U31#(tt(), V2) -> a__isNat# V2, a__U31#(tt(), V2) -> a__U32# a__isNat V2, mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> a__x#(mark X1, mark X2), mark# U11(X1, X2) -> a__U11#(mark X1, X2), mark# U11(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X, mark# U12 X -> mark# X, mark# isNat X -> a__isNat# X, mark# U21 X -> a__U21# mark X, mark# U21 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2), mark# U31(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X, mark# U32 X -> mark# X, mark# U41(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2), mark# U51(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3), mark# U52(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3), mark# U61 X -> mark# X, mark# U61 X -> a__U61# mark X, mark# U71(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3), mark# U72(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3), a__U41#(tt(), N) -> mark# N, a__U52#(tt(), M, N) -> mark# N, a__U52#(tt(), M, N) -> mark# M, a__U52#(tt(), M, N) -> a__plus#(mark N, mark M), a__U51#(tt(), M, N) -> a__isNat# N, a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N), a__plus#(N, s M) -> a__isNat# M, a__plus#(N, s M) -> a__U51#(a__isNat M, M, N), a__plus#(N, 0()) -> a__isNat# N, a__plus#(N, 0()) -> a__U41#(a__isNat N, N), a__U72#(tt(), M, N) -> mark# N, a__U72#(tt(), M, N) -> mark# M, a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__U72#(tt(), M, N) -> a__x#(mark N, mark M), a__U71#(tt(), M, N) -> a__isNat# N, a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N), a__x#(N, s M) -> a__isNat# M, a__x#(N, s M) -> a__U71#(a__isNat M, M, N), a__x#(N, 0()) -> a__isNat# N, a__x#(N, 0()) -> a__U61# a__isNat N} TRS: { a__U12 X -> U12 X, a__U12 tt() -> tt(), a__isNat X -> isNat X, a__isNat s V1 -> a__U21 a__isNat V1, a__isNat 0() -> tt(), a__isNat plus(V1, V2) -> a__U11(a__isNat V1, V2), a__isNat x(V1, V2) -> a__U31(a__isNat V1, V2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), V2) -> a__U12 a__isNat V2, a__U21 X -> U21 X, a__U21 tt() -> tt(), a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V2) -> a__U32 a__isNat V2, mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark x(X1, X2) -> a__x(mark X1, mark X2), mark U11(X1, X2) -> a__U11(mark X1, X2), mark U12 X -> a__U12 mark X, mark isNat X -> a__isNat X, mark U21 X -> a__U21 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41(X1, X2) -> a__U41(mark X1, X2), mark U51(X1, X2, X3) -> a__U51(mark X1, X2, X3), mark U52(X1, X2, X3) -> a__U52(mark X1, X2, X3), mark U61 X -> a__U61 mark X, mark U71(X1, X2, X3) -> a__U71(mark X1, X2, X3), mark U72(X1, X2, X3) -> a__U72(mark X1, X2, X3), a__U41(X1, X2) -> U41(X1, X2), a__U41(tt(), N) -> mark N, a__U52(X1, X2, X3) -> U52(X1, X2, X3), a__U52(tt(), M, N) -> s a__plus(mark N, mark M), a__U51(X1, X2, X3) -> U51(X1, X2, X3), a__U51(tt(), M, N) -> a__U52(a__isNat N, M, N), a__plus(N, s M) -> a__U51(a__isNat M, M, N), a__plus(N, 0()) -> a__U41(a__isNat N, N), a__plus(X1, X2) -> plus(X1, X2), a__U61 X -> U61 X, a__U61 tt() -> 0(), a__U72(X1, X2, X3) -> U72(X1, X2, X3), a__U72(tt(), M, N) -> a__plus(a__x(mark N, mark M), mark N), a__U71(X1, X2, X3) -> U71(X1, X2, X3), a__U71(tt(), M, N) -> a__U72(a__isNat N, M, N), a__x(N, s M) -> a__U71(a__isNat M, M, N), a__x(N, 0()) -> a__U61 a__isNat N, a__x(X1, X2) -> x(X1, X2)} UR: { a__U12 X -> U12 X, a__U12 tt() -> tt(), a__isNat X -> isNat X, a__isNat s V1 -> a__U21 a__isNat V1, a__isNat 0() -> tt(), a__isNat plus(V1, V2) -> a__U11(a__isNat V1, V2), a__isNat x(V1, V2) -> a__U31(a__isNat V1, V2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), V2) -> a__U12 a__isNat V2, a__U21 X -> U21 X, a__U21 tt() -> tt(), a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V2) -> a__U32 a__isNat V2, mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark x(X1, X2) -> a__x(mark X1, mark X2), mark U11(X1, X2) -> a__U11(mark X1, X2), mark U12 X -> a__U12 mark X, mark isNat X -> a__isNat X, mark U21 X -> a__U21 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41(X1, X2) -> a__U41(mark X1, X2), mark U51(X1, X2, X3) -> a__U51(mark X1, X2, X3), mark U52(X1, X2, X3) -> a__U52(mark X1, X2, X3), mark U61 X -> a__U61 mark X, mark U71(X1, X2, X3) -> a__U71(mark X1, X2, X3), mark U72(X1, X2, X3) -> a__U72(mark X1, X2, X3), a__U41(X1, X2) -> U41(X1, X2), a__U41(tt(), N) -> mark N, a__U52(X1, X2, X3) -> U52(X1, X2, X3), a__U52(tt(), M, N) -> s a__plus(mark N, mark M), a__U51(X1, X2, X3) -> U51(X1, X2, X3), a__U51(tt(), M, N) -> a__U52(a__isNat N, M, N), a__plus(N, s M) -> a__U51(a__isNat M, M, N), a__plus(N, 0()) -> a__U41(a__isNat N, N), a__plus(X1, X2) -> plus(X1, X2), a__U61 X -> U61 X, a__U61 tt() -> 0(), a__U72(X1, X2, X3) -> U72(X1, X2, X3), a__U72(tt(), M, N) -> a__plus(a__x(mark N, mark M), mark N), a__U71(X1, X2, X3) -> U71(X1, X2, X3), a__U71(tt(), M, N) -> a__U72(a__isNat N, M, N), a__x(N, s M) -> a__U71(a__isNat M, M, N), a__x(N, 0()) -> a__U61 a__isNat N, a__x(X1, X2) -> x(X1, X2)} EDG: { (mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__x#(N, 0()) -> a__U61# a__isNat N) (mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__x#(N, 0()) -> a__isNat# N) (mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__x#(N, s M) -> a__U71#(a__isNat M, M, N)) (mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__x#(N, s M) -> a__isNat# M) (a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, 0()) -> a__U41#(a__isNat N, N)) (a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, 0()) -> a__isNat# N) (a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, s M) -> a__U51#(a__isNat M, M, N)) (a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, s M) -> a__isNat# M) (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# x(V1, V2) -> a__isNat# V1) (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21# a__isNat V1) (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__isNat# V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__isNat# s V1 -> a__isNat# V1, a__isNat# x(V1, V2) -> a__isNat# V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__isNat# s V1 -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# s V1 -> a__U21# a__isNat V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# x(V1, V2) -> a__isNat# V1) (a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21# a__isNat V1) (a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (mark# U12 X -> mark# X, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U12 X -> mark# X, mark# U72(X1, X2, X3) -> mark# X1) (mark# U12 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U12 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U12 X -> mark# X, mark# U61 X -> a__U61# mark X) (mark# U12 X -> mark# X, mark# U61 X -> mark# X) (mark# U12 X -> mark# X, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U12 X -> mark# X, mark# U52(X1, X2, X3) -> mark# X1) (mark# U12 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U12 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U12 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U12 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U32 X -> mark# X) (mark# U12 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U12 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U12 X -> mark# X, mark# U21 X -> mark# X) (mark# U12 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U12 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U12 X -> mark# X, mark# U12 X -> mark# X) (mark# U12 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U12 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U12 X -> mark# X, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U12 X -> mark# X, mark# x(X1, X2) -> mark# X2) (mark# U12 X -> mark# X, mark# x(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U12 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U12 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# s X -> mark# X) (mark# U21 X -> mark# X, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U21 X -> mark# X, mark# U72(X1, X2, X3) -> mark# X1) (mark# U21 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U21 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U21 X -> mark# X, mark# U61 X -> a__U61# mark X) (mark# U21 X -> mark# X, mark# U61 X -> mark# X) (mark# U21 X -> mark# X, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U21 X -> mark# X, mark# U52(X1, X2, X3) -> mark# X1) (mark# U21 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U21 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U21 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U21 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# U32 X -> mark# X) (mark# U21 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U21 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U21 X -> mark# X, mark# U21 X -> mark# X) (mark# U21 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U21 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U21 X -> mark# X, mark# U12 X -> mark# X) (mark# U21 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U21 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U21 X -> mark# X, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U21 X -> mark# X, mark# x(X1, X2) -> mark# X2) (mark# U21 X -> mark# X, mark# x(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U21 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U21 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# s X -> mark# X) (mark# U61 X -> mark# X, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U61 X -> mark# X, mark# U72(X1, X2, X3) -> mark# X1) (mark# U61 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U61 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U61 X -> mark# X, mark# U61 X -> a__U61# mark X) (mark# U61 X -> mark# X, mark# U61 X -> mark# X) (mark# U61 X -> mark# X, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U61 X -> mark# X, mark# U52(X1, X2, X3) -> mark# X1) (mark# U61 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U61 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U61 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U61 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U61 X -> mark# X, mark# U32 X -> mark# X) (mark# U61 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U61 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U61 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U61 X -> mark# X, mark# U21 X -> mark# X) (mark# U61 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U61 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U61 X -> mark# X, mark# U12 X -> mark# X) (mark# U61 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U61 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U61 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U61 X -> mark# X, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U61 X -> mark# X, mark# x(X1, X2) -> mark# X2) (mark# U61 X -> mark# X, mark# x(X1, X2) -> mark# X1) (mark# U61 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U61 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U61 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U61 X -> mark# X, mark# s X -> mark# X) (a__U52#(tt(), M, N) -> mark# N, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# N, mark# U72(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# N, mark# U71(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U61 X -> a__U61# mark X) (a__U52#(tt(), M, N) -> mark# N, mark# U61 X -> mark# X) (a__U52#(tt(), M, N) -> mark# N, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# N, mark# U52(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# N, mark# U51(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (a__U52#(tt(), M, N) -> mark# N, mark# U41(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U32 X -> mark# X) (a__U52#(tt(), M, N) -> mark# N, mark# U32 X -> a__U32# mark X) (a__U52#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U52#(tt(), M, N) -> mark# N, mark# U21 X -> mark# X) (a__U52#(tt(), M, N) -> mark# N, mark# U21 X -> a__U21# mark X) (a__U52#(tt(), M, N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U52#(tt(), M, N) -> mark# N, mark# U12 X -> mark# X) (a__U52#(tt(), M, N) -> mark# N, mark# U12 X -> a__U12# mark X) (a__U52#(tt(), M, N) -> mark# N, mark# U11(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U52#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U52#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__U52#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U52#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U52#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# x(V1, V2) -> a__isNat# V1) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__U21# a__isNat V1) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1) (a__U71#(tt(), M, N) -> a__isNat# N, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__U71#(tt(), M, N) -> a__isNat# N, a__isNat# x(V1, V2) -> a__isNat# V1) (a__U71#(tt(), M, N) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__U71#(tt(), M, N) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__U71#(tt(), M, N) -> a__isNat# N, a__isNat# s V1 -> a__U21# a__isNat V1) (a__U71#(tt(), M, N) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1) (mark# plus(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U61 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# plus(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# plus(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U11(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U11(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U61 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U11(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U11(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U11(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U11(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U11(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U11(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U41(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U41(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U61 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U41(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U41(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U41(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U41(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U41(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U41(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U41(X1, X2) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U41(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U41(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U41(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U41(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U52(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U52(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U61 X -> mark# X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U52(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U52(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U52(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U52(X1, X2, X3) -> mark# X1, mark# U21 X -> mark# X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U52(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U52(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U52(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U52(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U52(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U52(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U72(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U72(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U61 X -> mark# X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U72(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U72(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U72(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U72(X1, X2, X3) -> mark# X1, mark# U21 X -> mark# X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U72(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U72(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U72(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U72(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U72(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U72(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (a__plus#(N, s M) -> a__U51#(a__isNat M, M, N), a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N)) (a__plus#(N, s M) -> a__U51#(a__isNat M, M, N), a__U51#(tt(), M, N) -> a__isNat# N) (a__x#(N, s M) -> a__U71#(a__isNat M, M, N), a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N)) (a__x#(N, s M) -> a__U71#(a__isNat M, M, N), a__U71#(tt(), M, N) -> a__isNat# N) (mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3), a__U52#(tt(), M, N) -> a__plus#(mark N, mark M)) (mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3), a__U52#(tt(), M, N) -> mark# M) (mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3), a__U52#(tt(), M, N) -> mark# N) (mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3), a__U72#(tt(), M, N) -> a__x#(mark N, mark M)) (mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3), a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N)) (mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3), a__U72#(tt(), M, N) -> mark# M) (mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3), a__U72#(tt(), M, N) -> mark# N) (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), V2) -> a__U32# a__isNat V2) (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), V2) -> a__isNat# V2) (a__plus#(N, 0()) -> a__U41#(a__isNat N, N), a__U41#(tt(), N) -> mark# N) (a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2), a__U31#(tt(), V2) -> a__U32# a__isNat V2) (a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2), a__U31#(tt(), V2) -> a__isNat# V2) (a__plus#(N, s M) -> a__isNat# M, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# x(V1, V2) -> a__isNat# V1) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__plus#(N, s M) -> a__isNat# M, a__isNat# s V1 -> a__U21# a__isNat V1) (a__plus#(N, s M) -> a__isNat# M, a__isNat# s V1 -> a__isNat# V1) (a__x#(N, s M) -> a__isNat# M, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__x#(N, s M) -> a__isNat# M, a__isNat# x(V1, V2) -> a__isNat# V1) (a__x#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__x#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__x#(N, s M) -> a__isNat# M, a__isNat# s V1 -> a__U21# a__isNat V1) (a__x#(N, s M) -> a__isNat# M, a__isNat# s V1 -> a__isNat# V1) (mark# x(X1, X2) -> mark# X2, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U72(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U71(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U61 X -> a__U61# mark X) (mark# x(X1, X2) -> mark# X2, mark# U61 X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U52(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U51(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# x(X1, X2) -> mark# X2, mark# U41(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U32 X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# U32 X -> a__U32# mark X) (mark# x(X1, X2) -> mark# X2, mark# U31(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# x(X1, X2) -> mark# X2, mark# U21 X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# U21 X -> a__U21# mark X) (mark# x(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (mark# x(X1, X2) -> mark# X2, mark# U12 X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# U12 X -> a__U12# mark X) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U12 X -> a__U12# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U12 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (mark# plus(X1, X2) -> mark# X2, mark# U21 X -> a__U21# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U21 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U32 X -> a__U32# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U32 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U51(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U52(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U61 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U61 X -> a__U61# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U71(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U72(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (a__U72#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U72#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U72#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X2) (a__U72#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U72#(tt(), M, N) -> mark# M, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U72#(tt(), M, N) -> mark# M, mark# U11(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U12 X -> a__U12# mark X) (a__U72#(tt(), M, N) -> mark# M, mark# U12 X -> mark# X) (a__U72#(tt(), M, N) -> mark# M, mark# isNat X -> a__isNat# X) (a__U72#(tt(), M, N) -> mark# M, mark# U21 X -> a__U21# mark X) (a__U72#(tt(), M, N) -> mark# M, mark# U21 X -> mark# X) (a__U72#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U72#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U32 X -> a__U32# mark X) (a__U72#(tt(), M, N) -> mark# M, mark# U32 X -> mark# X) (a__U72#(tt(), M, N) -> mark# M, mark# U41(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (a__U72#(tt(), M, N) -> mark# M, mark# U51(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# M, mark# U52(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# M, mark# U61 X -> mark# X) (a__U72#(tt(), M, N) -> mark# M, mark# U61 X -> a__U61# mark X) (a__U72#(tt(), M, N) -> mark# M, mark# U71(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# M, mark# U72(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (a__U52#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U52#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U52#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X2) (a__U52#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U52#(tt(), M, N) -> mark# M, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U52#(tt(), M, N) -> mark# M, mark# U11(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U12 X -> a__U12# mark X) (a__U52#(tt(), M, N) -> mark# M, mark# U12 X -> mark# X) (a__U52#(tt(), M, N) -> mark# M, mark# isNat X -> a__isNat# X) (a__U52#(tt(), M, N) -> mark# M, mark# U21 X -> a__U21# mark X) (a__U52#(tt(), M, N) -> mark# M, mark# U21 X -> mark# X) (a__U52#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U52#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U32 X -> a__U32# mark X) (a__U52#(tt(), M, N) -> mark# M, mark# U32 X -> mark# X) (a__U52#(tt(), M, N) -> mark# M, mark# U41(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (a__U52#(tt(), M, N) -> mark# M, mark# U51(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# M, mark# U52(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# M, mark# U61 X -> mark# X) (a__U52#(tt(), M, N) -> mark# M, mark# U61 X -> a__U61# mark X) (a__U52#(tt(), M, N) -> mark# M, mark# U71(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# M, mark# U72(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2), a__U11#(tt(), V2) -> a__U12# a__isNat V2) (a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2), a__U11#(tt(), V2) -> a__isNat# V2) (mark# U41(X1, X2) -> a__U41#(mark X1, X2), a__U41#(tt(), N) -> mark# N) (mark# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), V2) -> a__U12# a__isNat V2) (mark# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), V2) -> a__isNat# V2) (mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3), a__U71#(tt(), M, N) -> a__isNat# N) (mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3), a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N)) (mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3), a__U51#(tt(), M, N) -> a__isNat# N) (mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3), a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N)) (a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N), a__U72#(tt(), M, N) -> mark# N) (a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N), a__U72#(tt(), M, N) -> mark# M) (a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N), a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N)) (a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N), a__U72#(tt(), M, N) -> a__x#(mark N, mark M)) (a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N), a__U52#(tt(), M, N) -> mark# N) (a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N), a__U52#(tt(), M, N) -> mark# M) (a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N), a__U52#(tt(), M, N) -> a__plus#(mark N, mark M)) (mark# U71(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U71(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U71(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U21 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U61 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U51(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U51(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U51(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U21 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U61 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U31(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U31(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U31(X1, X2) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U31(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U31(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (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# U32 X -> a__U32# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U61 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# x(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# x(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# x(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# x(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# x(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# x(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U61 X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# x(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__x#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1) (a__x#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__U21# a__isNat V1) (a__x#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__x#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__x#(N, 0()) -> a__isNat# N, a__isNat# x(V1, V2) -> a__isNat# V1) (a__x#(N, 0()) -> a__isNat# N, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__U72#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__U72#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U72#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U72#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__U72#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U72#(tt(), M, N) -> mark# N, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U72#(tt(), M, N) -> mark# N, mark# U11(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U12 X -> a__U12# mark X) (a__U72#(tt(), M, N) -> mark# N, mark# U12 X -> mark# X) (a__U72#(tt(), M, N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U72#(tt(), M, N) -> mark# N, mark# U21 X -> a__U21# mark X) (a__U72#(tt(), M, N) -> mark# N, mark# U21 X -> mark# X) (a__U72#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U72#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U32 X -> a__U32# mark X) (a__U72#(tt(), M, N) -> mark# N, mark# U32 X -> mark# X) (a__U72#(tt(), M, N) -> mark# N, mark# U41(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (a__U72#(tt(), M, N) -> mark# N, mark# U51(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# N, mark# U52(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# N, mark# U61 X -> mark# X) (a__U72#(tt(), M, N) -> mark# N, mark# U61 X -> a__U61# mark X) (a__U72#(tt(), M, N) -> mark# N, mark# U71(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# N, mark# U72(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__U51#(tt(), M, N) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1) (a__U51#(tt(), M, N) -> a__isNat# N, a__isNat# s V1 -> a__U21# a__isNat V1) (a__U51#(tt(), M, N) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__U51#(tt(), M, N) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__U51#(tt(), M, N) -> a__isNat# N, a__isNat# x(V1, V2) -> a__isNat# V1) (a__U51#(tt(), M, N) -> a__isNat# N, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__U41#(tt(), N) -> mark# N, mark# s X -> mark# X) (a__U41#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U41#(tt(), N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U41#(tt(), N) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__U41#(tt(), N) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U41#(tt(), N) -> mark# N, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U41#(tt(), N) -> mark# N, mark# U11(X1, X2) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U12 X -> a__U12# mark X) (a__U41#(tt(), N) -> mark# N, mark# U12 X -> mark# X) (a__U41#(tt(), N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U41#(tt(), N) -> mark# N, mark# U21 X -> a__U21# mark X) (a__U41#(tt(), N) -> mark# N, mark# U21 X -> mark# X) (a__U41#(tt(), N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U41#(tt(), N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U32 X -> a__U32# mark X) (a__U41#(tt(), N) -> mark# N, mark# U32 X -> mark# X) (a__U41#(tt(), N) -> mark# N, mark# U41(X1, X2) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (a__U41#(tt(), N) -> mark# N, mark# U51(X1, X2, X3) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__U41#(tt(), N) -> mark# N, mark# U52(X1, X2, X3) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (a__U41#(tt(), N) -> mark# N, mark# U61 X -> mark# X) (a__U41#(tt(), N) -> mark# N, mark# U61 X -> a__U61# mark X) (a__U41#(tt(), N) -> mark# N, mark# U71(X1, X2, X3) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (a__U41#(tt(), N) -> mark# N, mark# U72(X1, X2, X3) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# s X -> mark# X) (mark# U32 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U32 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U32 X -> mark# X, mark# x(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# x(X1, X2) -> mark# X2) (mark# U32 X -> mark# X, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U32 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U32 X -> mark# X, mark# U12 X -> mark# X) (mark# U32 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U32 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U32 X -> mark# X, mark# U21 X -> mark# X) (mark# U32 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U32 X -> mark# X, mark# U32 X -> mark# X) (mark# U32 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U52(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U61 X -> mark# X) (mark# U32 X -> mark# X, mark# U61 X -> a__U61# mark X) (mark# U32 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U72(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__isNat# V1) (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__U21# a__isNat V1) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__isNat# V1) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (mark# isNat X -> a__isNat# X, a__isNat# x(V1, V2) -> a__isNat# V1) (mark# isNat X -> a__isNat# X, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (mark# s X -> mark# X, mark# s X -> mark# 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# x(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# x(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# s X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# s X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# s X -> mark# X, mark# U12 X -> mark# X) (mark# s X -> mark# X, mark# isNat X -> a__isNat# X) (mark# s X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# s X -> mark# X, mark# U21 X -> mark# X) (mark# s X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# s X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# s X -> mark# X, mark# U32 X -> mark# X) (mark# s X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# s X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U52(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U61 X -> mark# X) (mark# s X -> mark# X, mark# U61 X -> a__U61# mark X) (mark# s X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U72(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21# a__isNat V1) (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# x(V1, V2) -> a__isNat# V1) (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__U31#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__isNat# V1) (a__U31#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21# a__isNat V1) (a__U31#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__U31#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__U31#(tt(), V2) -> a__isNat# V2, a__isNat# x(V1, V2) -> a__isNat# V1) (a__U31#(tt(), V2) -> a__isNat# V2, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__U72#(tt(), M, N) -> a__x#(mark N, mark M), a__x#(N, s M) -> a__isNat# M) (a__U72#(tt(), M, N) -> a__x#(mark N, mark M), a__x#(N, s M) -> a__U71#(a__isNat M, M, N)) (a__U72#(tt(), M, N) -> a__x#(mark N, mark M), a__x#(N, 0()) -> a__isNat# N) (a__U72#(tt(), M, N) -> a__x#(mark N, mark M), a__x#(N, 0()) -> a__U61# a__isNat N) (a__U52#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__isNat# M) (a__U52#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U51#(a__isNat M, M, N)) (a__U52#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__isNat# N) (a__U52#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__U41#(a__isNat N, N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__isNat# M) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__U51#(a__isNat M, M, 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, 0()) -> a__U41#(a__isNat N, N)) } EDG: { (mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__x#(N, 0()) -> a__U61# a__isNat N) (mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__x#(N, 0()) -> a__isNat# N) (mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__x#(N, s M) -> a__U71#(a__isNat M, M, N)) (mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__x#(N, s M) -> a__isNat# M) (a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, 0()) -> a__U41#(a__isNat N, N)) (a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, 0()) -> a__isNat# N) (a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, s M) -> a__U51#(a__isNat M, M, N)) (a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, s M) -> a__isNat# M) (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# x(V1, V2) -> a__isNat# V1) (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21# a__isNat V1) (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__isNat# V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__isNat# s V1 -> a__isNat# V1, a__isNat# x(V1, V2) -> a__isNat# V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__isNat# s V1 -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# s V1 -> a__U21# a__isNat V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# x(V1, V2) -> a__isNat# V1) (a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21# a__isNat V1) (a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (mark# U12 X -> mark# X, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U12 X -> mark# X, mark# U72(X1, X2, X3) -> mark# X1) (mark# U12 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U12 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U12 X -> mark# X, mark# U61 X -> a__U61# mark X) (mark# U12 X -> mark# X, mark# U61 X -> mark# X) (mark# U12 X -> mark# X, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U12 X -> mark# X, mark# U52(X1, X2, X3) -> mark# X1) (mark# U12 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U12 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U12 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U12 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U32 X -> mark# X) (mark# U12 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U12 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U12 X -> mark# X, mark# U21 X -> mark# X) (mark# U12 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U12 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U12 X -> mark# X, mark# U12 X -> mark# X) (mark# U12 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U12 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U12 X -> mark# X, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U12 X -> mark# X, mark# x(X1, X2) -> mark# X2) (mark# U12 X -> mark# X, mark# x(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U12 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U12 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# s X -> mark# X) (mark# U21 X -> mark# X, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U21 X -> mark# X, mark# U72(X1, X2, X3) -> mark# X1) (mark# U21 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U21 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U21 X -> mark# X, mark# U61 X -> a__U61# mark X) (mark# U21 X -> mark# X, mark# U61 X -> mark# X) (mark# U21 X -> mark# X, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U21 X -> mark# X, mark# U52(X1, X2, X3) -> mark# X1) (mark# U21 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U21 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U21 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U21 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# U32 X -> mark# X) (mark# U21 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U21 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U21 X -> mark# X, mark# U21 X -> mark# X) (mark# U21 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U21 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U21 X -> mark# X, mark# U12 X -> mark# X) (mark# U21 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U21 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U21 X -> mark# X, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U21 X -> mark# X, mark# x(X1, X2) -> mark# X2) (mark# U21 X -> mark# X, mark# x(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U21 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U21 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U21 X -> mark# X, mark# s X -> mark# X) (mark# U61 X -> mark# X, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U61 X -> mark# X, mark# U72(X1, X2, X3) -> mark# X1) (mark# U61 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U61 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U61 X -> mark# X, mark# U61 X -> a__U61# mark X) (mark# U61 X -> mark# X, mark# U61 X -> mark# X) (mark# U61 X -> mark# X, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U61 X -> mark# X, mark# U52(X1, X2, X3) -> mark# X1) (mark# U61 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U61 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U61 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U61 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U61 X -> mark# X, mark# U32 X -> mark# X) (mark# U61 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U61 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U61 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U61 X -> mark# X, mark# U21 X -> mark# X) (mark# U61 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U61 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U61 X -> mark# X, mark# U12 X -> mark# X) (mark# U61 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U61 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U61 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U61 X -> mark# X, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U61 X -> mark# X, mark# x(X1, X2) -> mark# X2) (mark# U61 X -> mark# X, mark# x(X1, X2) -> mark# X1) (mark# U61 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U61 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U61 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U61 X -> mark# X, mark# s X -> mark# X) (a__U52#(tt(), M, N) -> mark# N, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# N, mark# U72(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# N, mark# U71(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U61 X -> a__U61# mark X) (a__U52#(tt(), M, N) -> mark# N, mark# U61 X -> mark# X) (a__U52#(tt(), M, N) -> mark# N, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# N, mark# U52(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# N, mark# U51(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (a__U52#(tt(), M, N) -> mark# N, mark# U41(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U32 X -> mark# X) (a__U52#(tt(), M, N) -> mark# N, mark# U32 X -> a__U32# mark X) (a__U52#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U52#(tt(), M, N) -> mark# N, mark# U21 X -> mark# X) (a__U52#(tt(), M, N) -> mark# N, mark# U21 X -> a__U21# mark X) (a__U52#(tt(), M, N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U52#(tt(), M, N) -> mark# N, mark# U12 X -> mark# X) (a__U52#(tt(), M, N) -> mark# N, mark# U12 X -> a__U12# mark X) (a__U52#(tt(), M, N) -> mark# N, mark# U11(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U52#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U52#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__U52#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U52#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U52#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# x(V1, V2) -> a__isNat# V1) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__U21# a__isNat V1) (a__plus#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1) (a__U71#(tt(), M, N) -> a__isNat# N, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__U71#(tt(), M, N) -> a__isNat# N, a__isNat# x(V1, V2) -> a__isNat# V1) (a__U71#(tt(), M, N) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__U71#(tt(), M, N) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__U71#(tt(), M, N) -> a__isNat# N, a__isNat# s V1 -> a__U21# a__isNat V1) (a__U71#(tt(), M, N) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1) (mark# plus(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U61 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# plus(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# plus(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U11(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U11(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U61 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U11(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U11(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U11(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U11(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U11(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U11(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U41(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U41(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U61 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U41(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U41(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U41(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U41(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U41(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U41(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U41(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U41(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U41(X1, X2) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U41(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U41(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U41(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U41(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U41(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U52(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U52(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U61 X -> mark# X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U52(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U52(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U52(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U52(X1, X2, X3) -> mark# X1, mark# U21 X -> mark# X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U52(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U52(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U52(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U52(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U52(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U52(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U52(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U52(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U72(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U72(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U61 X -> mark# X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U72(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U72(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U72(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U72(X1, X2, X3) -> mark# X1, mark# U21 X -> mark# X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U72(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U72(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U72(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U72(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U72(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U72(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U72(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U72(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (a__plus#(N, s M) -> a__U51#(a__isNat M, M, N), a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N)) (a__plus#(N, s M) -> a__U51#(a__isNat M, M, N), a__U51#(tt(), M, N) -> a__isNat# N) (a__x#(N, s M) -> a__U71#(a__isNat M, M, N), a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N)) (a__x#(N, s M) -> a__U71#(a__isNat M, M, N), a__U71#(tt(), M, N) -> a__isNat# N) (mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3), a__U52#(tt(), M, N) -> a__plus#(mark N, mark M)) (mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3), a__U52#(tt(), M, N) -> mark# M) (mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3), a__U52#(tt(), M, N) -> mark# N) (mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3), a__U72#(tt(), M, N) -> a__x#(mark N, mark M)) (mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3), a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N)) (mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3), a__U72#(tt(), M, N) -> mark# M) (mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3), a__U72#(tt(), M, N) -> mark# N) (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), V2) -> a__U32# a__isNat V2) (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), V2) -> a__isNat# V2) (a__plus#(N, 0()) -> a__U41#(a__isNat N, N), a__U41#(tt(), N) -> mark# N) (a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2), a__U31#(tt(), V2) -> a__U32# a__isNat V2) (a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2), a__U31#(tt(), V2) -> a__isNat# V2) (a__plus#(N, s M) -> a__isNat# M, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# x(V1, V2) -> a__isNat# V1) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__plus#(N, s M) -> a__isNat# M, a__isNat# s V1 -> a__U21# a__isNat V1) (a__plus#(N, s M) -> a__isNat# M, a__isNat# s V1 -> a__isNat# V1) (a__x#(N, s M) -> a__isNat# M, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__x#(N, s M) -> a__isNat# M, a__isNat# x(V1, V2) -> a__isNat# V1) (a__x#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__x#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__x#(N, s M) -> a__isNat# M, a__isNat# s V1 -> a__U21# a__isNat V1) (a__x#(N, s M) -> a__isNat# M, a__isNat# s V1 -> a__isNat# V1) (mark# x(X1, X2) -> mark# X2, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U72(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U71(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U61 X -> a__U61# mark X) (mark# x(X1, X2) -> mark# X2, mark# U61 X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U52(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U51(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# x(X1, X2) -> mark# X2, mark# U41(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U32 X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# U32 X -> a__U32# mark X) (mark# x(X1, X2) -> mark# X2, mark# U31(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# x(X1, X2) -> mark# X2, mark# U21 X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# U21 X -> a__U21# mark X) (mark# x(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (mark# x(X1, X2) -> mark# X2, mark# U12 X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# U12 X -> a__U12# mark X) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U12 X -> a__U12# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U12 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (mark# plus(X1, X2) -> mark# X2, mark# U21 X -> a__U21# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U21 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U32 X -> a__U32# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U32 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U51(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U52(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U61 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U61 X -> a__U61# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U71(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U72(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (a__U72#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U72#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U72#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X2) (a__U72#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U72#(tt(), M, N) -> mark# M, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U72#(tt(), M, N) -> mark# M, mark# U11(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U12 X -> a__U12# mark X) (a__U72#(tt(), M, N) -> mark# M, mark# U12 X -> mark# X) (a__U72#(tt(), M, N) -> mark# M, mark# isNat X -> a__isNat# X) (a__U72#(tt(), M, N) -> mark# M, mark# U21 X -> a__U21# mark X) (a__U72#(tt(), M, N) -> mark# M, mark# U21 X -> mark# X) (a__U72#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U72#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U32 X -> a__U32# mark X) (a__U72#(tt(), M, N) -> mark# M, mark# U32 X -> mark# X) (a__U72#(tt(), M, N) -> mark# M, mark# U41(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (a__U72#(tt(), M, N) -> mark# M, mark# U51(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# M, mark# U52(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# M, mark# U61 X -> mark# X) (a__U72#(tt(), M, N) -> mark# M, mark# U61 X -> a__U61# mark X) (a__U72#(tt(), M, N) -> mark# M, mark# U71(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# M, mark# U72(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# M, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (a__U52#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U52#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U52#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X2) (a__U52#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U52#(tt(), M, N) -> mark# M, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U52#(tt(), M, N) -> mark# M, mark# U11(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U12 X -> a__U12# mark X) (a__U52#(tt(), M, N) -> mark# M, mark# U12 X -> mark# X) (a__U52#(tt(), M, N) -> mark# M, mark# isNat X -> a__isNat# X) (a__U52#(tt(), M, N) -> mark# M, mark# U21 X -> a__U21# mark X) (a__U52#(tt(), M, N) -> mark# M, mark# U21 X -> mark# X) (a__U52#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U52#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U32 X -> a__U32# mark X) (a__U52#(tt(), M, N) -> mark# M, mark# U32 X -> mark# X) (a__U52#(tt(), M, N) -> mark# M, mark# U41(X1, X2) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (a__U52#(tt(), M, N) -> mark# M, mark# U51(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# M, mark# U52(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# M, mark# U61 X -> mark# X) (a__U52#(tt(), M, N) -> mark# M, mark# U61 X -> a__U61# mark X) (a__U52#(tt(), M, N) -> mark# M, mark# U71(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (a__U52#(tt(), M, N) -> mark# M, mark# U72(X1, X2, X3) -> mark# X1) (a__U52#(tt(), M, N) -> mark# M, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2), a__U11#(tt(), V2) -> a__U12# a__isNat V2) (a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2), a__U11#(tt(), V2) -> a__isNat# V2) (mark# U41(X1, X2) -> a__U41#(mark X1, X2), a__U41#(tt(), N) -> mark# N) (mark# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), V2) -> a__U12# a__isNat V2) (mark# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), V2) -> a__isNat# V2) (mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3), a__U71#(tt(), M, N) -> a__isNat# N) (mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3), a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N)) (mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3), a__U51#(tt(), M, N) -> a__isNat# N) (mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3), a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N)) (a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N), a__U72#(tt(), M, N) -> mark# N) (a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N), a__U72#(tt(), M, N) -> mark# M) (a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N), a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N)) (a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N), a__U72#(tt(), M, N) -> a__x#(mark N, mark M)) (a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N), a__U52#(tt(), M, N) -> mark# N) (a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N), a__U52#(tt(), M, N) -> mark# M) (a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N), a__U52#(tt(), M, N) -> a__plus#(mark N, mark M)) (mark# U71(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U71(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U71(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U21 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U61 X -> mark# X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U71(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U71(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U71(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U51(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U51(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U51(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U21 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U61 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U31(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U31(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U31(X1, X2) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U31(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U31(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (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# U32 X -> a__U32# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U61 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# x(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# x(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X) (mark# x(X1, X2) -> mark# X1, mark# U21 X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# x(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# x(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# U41(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# x(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U61 X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# U61 X -> a__U61# mark X) (mark# x(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__x#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1) (a__x#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__U21# a__isNat V1) (a__x#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__x#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__x#(N, 0()) -> a__isNat# N, a__isNat# x(V1, V2) -> a__isNat# V1) (a__x#(N, 0()) -> a__isNat# N, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__U72#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__U72#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U72#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U72#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__U72#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U72#(tt(), M, N) -> mark# N, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U72#(tt(), M, N) -> mark# N, mark# U11(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U12 X -> a__U12# mark X) (a__U72#(tt(), M, N) -> mark# N, mark# U12 X -> mark# X) (a__U72#(tt(), M, N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U72#(tt(), M, N) -> mark# N, mark# U21 X -> a__U21# mark X) (a__U72#(tt(), M, N) -> mark# N, mark# U21 X -> mark# X) (a__U72#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U72#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U32 X -> a__U32# mark X) (a__U72#(tt(), M, N) -> mark# N, mark# U32 X -> mark# X) (a__U72#(tt(), M, N) -> mark# N, mark# U41(X1, X2) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (a__U72#(tt(), M, N) -> mark# N, mark# U51(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# N, mark# U52(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# N, mark# U61 X -> mark# X) (a__U72#(tt(), M, N) -> mark# N, mark# U61 X -> a__U61# mark X) (a__U72#(tt(), M, N) -> mark# N, mark# U71(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (a__U72#(tt(), M, N) -> mark# N, mark# U72(X1, X2, X3) -> mark# X1) (a__U72#(tt(), M, N) -> mark# N, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__U51#(tt(), M, N) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1) (a__U51#(tt(), M, N) -> a__isNat# N, a__isNat# s V1 -> a__U21# a__isNat V1) (a__U51#(tt(), M, N) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__U51#(tt(), M, N) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__U51#(tt(), M, N) -> a__isNat# N, a__isNat# x(V1, V2) -> a__isNat# V1) (a__U51#(tt(), M, N) -> a__isNat# N, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__U41#(tt(), N) -> mark# N, mark# s X -> mark# X) (a__U41#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U41#(tt(), N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U41#(tt(), N) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__U41#(tt(), N) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U41#(tt(), N) -> mark# N, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U41#(tt(), N) -> mark# N, mark# U11(X1, X2) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U12 X -> a__U12# mark X) (a__U41#(tt(), N) -> mark# N, mark# U12 X -> mark# X) (a__U41#(tt(), N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U41#(tt(), N) -> mark# N, mark# U21 X -> a__U21# mark X) (a__U41#(tt(), N) -> mark# N, mark# U21 X -> mark# X) (a__U41#(tt(), N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U41#(tt(), N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U32 X -> a__U32# mark X) (a__U41#(tt(), N) -> mark# N, mark# U32 X -> mark# X) (a__U41#(tt(), N) -> mark# N, mark# U41(X1, X2) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (a__U41#(tt(), N) -> mark# N, mark# U51(X1, X2, X3) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__U41#(tt(), N) -> mark# N, mark# U52(X1, X2, X3) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (a__U41#(tt(), N) -> mark# N, mark# U61 X -> mark# X) (a__U41#(tt(), N) -> mark# N, mark# U61 X -> a__U61# mark X) (a__U41#(tt(), N) -> mark# N, mark# U71(X1, X2, X3) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (a__U41#(tt(), N) -> mark# N, mark# U72(X1, X2, X3) -> mark# X1) (a__U41#(tt(), N) -> mark# N, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# s X -> mark# X) (mark# U32 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U32 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U32 X -> mark# X, mark# x(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# x(X1, X2) -> mark# X2) (mark# U32 X -> mark# X, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U32 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U32 X -> mark# X, mark# U12 X -> mark# X) (mark# U32 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U32 X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# U32 X -> mark# X, mark# U21 X -> mark# X) (mark# U32 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U32 X -> mark# X, mark# U32 X -> mark# X) (mark# U32 X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U52(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U61 X -> mark# X) (mark# U32 X -> mark# X, mark# U61 X -> a__U61# mark X) (mark# U32 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U72(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__isNat# V1) (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__U21# a__isNat V1) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__isNat# V1) (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (mark# isNat X -> a__isNat# X, a__isNat# x(V1, V2) -> a__isNat# V1) (mark# isNat X -> a__isNat# X, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (mark# s X -> mark# X, mark# s X -> mark# 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# x(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# x(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# s X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# s X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# s X -> mark# X, mark# U12 X -> mark# X) (mark# s X -> mark# X, mark# isNat X -> a__isNat# X) (mark# s X -> mark# X, mark# U21 X -> a__U21# mark X) (mark# s X -> mark# X, mark# U21 X -> mark# X) (mark# s X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# s X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# s X -> mark# X, mark# U32 X -> mark# X) (mark# s X -> mark# X, mark# U41(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U41(X1, X2) -> a__U41#(mark X1, X2)) (mark# s X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U52(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U61 X -> mark# X) (mark# s X -> mark# X, mark# U61 X -> a__U61# mark X) (mark# s X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U72(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3)) (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21# a__isNat V1) (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# x(V1, V2) -> a__isNat# V1) (a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__U31#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__isNat# V1) (a__U31#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21# a__isNat V1) (a__U31#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__isNat# V1) (a__U31#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2)) (a__U31#(tt(), V2) -> a__isNat# V2, a__isNat# x(V1, V2) -> a__isNat# V1) (a__U31#(tt(), V2) -> a__isNat# V2, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2)) (a__U72#(tt(), M, N) -> a__x#(mark N, mark M), a__x#(N, s M) -> a__isNat# M) (a__U72#(tt(), M, N) -> a__x#(mark N, mark M), a__x#(N, s M) -> a__U71#(a__isNat M, M, N)) (a__U72#(tt(), M, N) -> a__x#(mark N, mark M), a__x#(N, 0()) -> a__isNat# N) (a__U72#(tt(), M, N) -> a__x#(mark N, mark M), a__x#(N, 0()) -> a__U61# a__isNat N) (a__U52#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__isNat# M) (a__U52#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U51#(a__isNat M, M, N)) (a__U52#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__isNat# N) (a__U52#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__U41#(a__isNat N, N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__isNat# M) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__U51#(a__isNat M, M, 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, 0()) -> a__U41#(a__isNat N, N)) } STATUS: arrows: 0.790556 SCCS (2): Scc: { mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> a__x#(mark X1, mark X2), mark# U11(X1, X2) -> mark# X1, mark# U12 X -> mark# X, mark# U21 X -> mark# X, mark# U31(X1, X2) -> mark# X1, mark# U32 X -> mark# X, mark# U41(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2), mark# U51(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3), mark# U52(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3), mark# U61 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3), mark# U72(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3), a__U41#(tt(), N) -> mark# N, a__U52#(tt(), M, N) -> mark# N, a__U52#(tt(), M, N) -> mark# M, a__U52#(tt(), M, N) -> a__plus#(mark N, mark M), a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N), a__plus#(N, s M) -> a__U51#(a__isNat M, M, N), a__plus#(N, 0()) -> a__U41#(a__isNat N, N), a__U72#(tt(), M, N) -> mark# N, a__U72#(tt(), M, N) -> mark# M, a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__U72#(tt(), M, N) -> a__x#(mark N, mark M), a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N), a__x#(N, s M) -> a__U71#(a__isNat M, M, N)} Scc: { a__isNat# s V1 -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2), a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2), a__U11#(tt(), V2) -> a__isNat# V2, a__U31#(tt(), V2) -> a__isNat# V2} SCC (36): Strict: { mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> a__x#(mark X1, mark X2), mark# U11(X1, X2) -> mark# X1, mark# U12 X -> mark# X, mark# U21 X -> mark# X, mark# U31(X1, X2) -> mark# X1, mark# U32 X -> mark# X, mark# U41(X1, X2) -> mark# X1, mark# U41(X1, X2) -> a__U41#(mark X1, X2), mark# U51(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3), mark# U52(X1, X2, X3) -> mark# X1, mark# U52(X1, X2, X3) -> a__U52#(mark X1, X2, X3), mark# U61 X -> mark# X, mark# U71(X1, X2, X3) -> mark# X1, mark# U71(X1, X2, X3) -> a__U71#(mark X1, X2, X3), mark# U72(X1, X2, X3) -> mark# X1, mark# U72(X1, X2, X3) -> a__U72#(mark X1, X2, X3), a__U41#(tt(), N) -> mark# N, a__U52#(tt(), M, N) -> mark# N, a__U52#(tt(), M, N) -> mark# M, a__U52#(tt(), M, N) -> a__plus#(mark N, mark M), a__U51#(tt(), M, N) -> a__U52#(a__isNat N, M, N), a__plus#(N, s M) -> a__U51#(a__isNat M, M, N), a__plus#(N, 0()) -> a__U41#(a__isNat N, N), a__U72#(tt(), M, N) -> mark# N, a__U72#(tt(), M, N) -> mark# M, a__U72#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__U72#(tt(), M, N) -> a__x#(mark N, mark M), a__U71#(tt(), M, N) -> a__U72#(a__isNat N, M, N), a__x#(N, s M) -> a__U71#(a__isNat M, M, N)} Weak: { a__U12 X -> U12 X, a__U12 tt() -> tt(), a__isNat X -> isNat X, a__isNat s V1 -> a__U21 a__isNat V1, a__isNat 0() -> tt(), a__isNat plus(V1, V2) -> a__U11(a__isNat V1, V2), a__isNat x(V1, V2) -> a__U31(a__isNat V1, V2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), V2) -> a__U12 a__isNat V2, a__U21 X -> U21 X, a__U21 tt() -> tt(), a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V2) -> a__U32 a__isNat V2, mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark x(X1, X2) -> a__x(mark X1, mark X2), mark U11(X1, X2) -> a__U11(mark X1, X2), mark U12 X -> a__U12 mark X, mark isNat X -> a__isNat X, mark U21 X -> a__U21 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41(X1, X2) -> a__U41(mark X1, X2), mark U51(X1, X2, X3) -> a__U51(mark X1, X2, X3), mark U52(X1, X2, X3) -> a__U52(mark X1, X2, X3), mark U61 X -> a__U61 mark X, mark U71(X1, X2, X3) -> a__U71(mark X1, X2, X3), mark U72(X1, X2, X3) -> a__U72(mark X1, X2, X3), a__U41(X1, X2) -> U41(X1, X2), a__U41(tt(), N) -> mark N, a__U52(X1, X2, X3) -> U52(X1, X2, X3), a__U52(tt(), M, N) -> s a__plus(mark N, mark M), a__U51(X1, X2, X3) -> U51(X1, X2, X3), a__U51(tt(), M, N) -> a__U52(a__isNat N, M, N), a__plus(N, s M) -> a__U51(a__isNat M, M, N), a__plus(N, 0()) -> a__U41(a__isNat N, N), a__plus(X1, X2) -> plus(X1, X2), a__U61 X -> U61 X, a__U61 tt() -> 0(), a__U72(X1, X2, X3) -> U72(X1, X2, X3), a__U72(tt(), M, N) -> a__plus(a__x(mark N, mark M), mark N), a__U71(X1, X2, X3) -> U71(X1, X2, X3), a__U71(tt(), M, N) -> a__U72(a__isNat N, M, N), a__x(N, s M) -> a__U71(a__isNat M, M, N), a__x(N, 0()) -> a__U61 a__isNat N, a__x(X1, X2) -> x(X1, X2)} Open SCC (7): Strict: { a__isNat# s V1 -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2), a__isNat# x(V1, V2) -> a__isNat# V1, a__isNat# x(V1, V2) -> a__U31#(a__isNat V1, V2), a__U11#(tt(), V2) -> a__isNat# V2, a__U31#(tt(), V2) -> a__isNat# V2} Weak: { a__U12 X -> U12 X, a__U12 tt() -> tt(), a__isNat X -> isNat X, a__isNat s V1 -> a__U21 a__isNat V1, a__isNat 0() -> tt(), a__isNat plus(V1, V2) -> a__U11(a__isNat V1, V2), a__isNat x(V1, V2) -> a__U31(a__isNat V1, V2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), V2) -> a__U12 a__isNat V2, a__U21 X -> U21 X, a__U21 tt() -> tt(), a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V2) -> a__U32 a__isNat V2, mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark x(X1, X2) -> a__x(mark X1, mark X2), mark U11(X1, X2) -> a__U11(mark X1, X2), mark U12 X -> a__U12 mark X, mark isNat X -> a__isNat X, mark U21 X -> a__U21 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41(X1, X2) -> a__U41(mark X1, X2), mark U51(X1, X2, X3) -> a__U51(mark X1, X2, X3), mark U52(X1, X2, X3) -> a__U52(mark X1, X2, X3), mark U61 X -> a__U61 mark X, mark U71(X1, X2, X3) -> a__U71(mark X1, X2, X3), mark U72(X1, X2, X3) -> a__U72(mark X1, X2, X3), a__U41(X1, X2) -> U41(X1, X2), a__U41(tt(), N) -> mark N, a__U52(X1, X2, X3) -> U52(X1, X2, X3), a__U52(tt(), M, N) -> s a__plus(mark N, mark M), a__U51(X1, X2, X3) -> U51(X1, X2, X3), a__U51(tt(), M, N) -> a__U52(a__isNat N, M, N), a__plus(N, s M) -> a__U51(a__isNat M, M, N), a__plus(N, 0()) -> a__U41(a__isNat N, N), a__plus(X1, X2) -> plus(X1, X2), a__U61 X -> U61 X, a__U61 tt() -> 0(), a__U72(X1, X2, X3) -> U72(X1, X2, X3), a__U72(tt(), M, N) -> a__plus(a__x(mark N, mark M), mark N), a__U71(X1, X2, X3) -> U71(X1, X2, X3), a__U71(tt(), M, N) -> a__U72(a__isNat N, M, N), a__x(N, s M) -> a__U71(a__isNat M, M, N), a__x(N, 0()) -> a__U61 a__isNat N, a__x(X1, X2) -> x(X1, X2)} Open