YES Termination w.r.t. Q proof of Transformed_CSR_04_PEANO_complete_GM.ari

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
↳1 QTRSRRRProof (⇔, 165 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 0 ms)
↳4 QTRS
↳5 RisEmptyProof (⇔, 0 ms)
↳6 YES

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a__U11(tt, V1, V2) → a__U12(a__isNat(V1), V2)
a__U12(tt, V2) → a__U13(a__isNat(V2))
a__U13(tt) → tt
a__U21(tt, V1) → a__U22(a__isNat(V1))
a__U22(tt) → tt
a__U31(tt, N) → mark(N)
a__U41(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__and(tt, X) → mark(X)
a__isNat(0) → tt
a__isNat(plus(V1, V2)) → a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)
a__isNatKind(0) → tt
a__isNatKind(plus(V1, V2)) → a__and(a__isNatKind(V1), isNatKind(V2))
a__isNatKind(s(V1)) → a__isNatKind(V1)
a__plus(N, 0) → a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__plus(N, s(M)) → a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)
mark(U13(X)) → a__U13(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNatKind(X)) → a__isNatKind(X)
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)
a__U12(X1, X2) → U12(X1, X2)
a__isNat(X) → isNat(X)
a__U13(X) → U13(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__U31(X1, X2) → U31(X1, X2)
a__U41(X1, X2, X3) → U41(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNatKind(X) → isNatKind(X)

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Combined order from the following AFS and order.
a__U11(x1, x2, x3)  =  a__U11(x1, x2, x3)
tt  =  tt
a__U12(x1, x2)  =  a__U12(x1, x2)
a__isNat(x1)  =  x1
a__U13(x1)  =  x1
a__U21(x1, x2)  =  a__U21(x1, x2)
a__U22(x1)  =  x1
a__U31(x1, x2)  =  a__U31(x1, x2)
mark(x1)  =  x1
a__U41(x1, x2, x3)  =  a__U41(x1, x2, x3)
s(x1)  =  s(x1)
a__plus(x1, x2)  =  a__plus(x1, x2)
a__and(x1, x2)  =  a__and(x1, x2)
0  =  0
plus(x1, x2)  =  plus(x1, x2)
a__isNatKind(x1)  =  x1
isNatKind(x1)  =  x1
and(x1, x2)  =  and(x1, x2)
isNat(x1)  =  x1
U11(x1, x2, x3)  =  U11(x1, x2, x3)
U12(x1, x2)  =  U12(x1, x2)
U13(x1)  =  x1
U21(x1, x2)  =  U21(x1, x2)
U22(x1)  =  x1
U31(x1, x2)  =  U31(x1, x2)
U41(x1, x2, x3)  =  U41(x1, x2, x3)

Recursive path order with status [RPO].
Quasi-Precedence:
[tt, 0] > [aU413, aplus2, plus2, U413] > [aU113, U113] > [aU122, U122] > [aU212, U212]
[tt, 0] > [aU413, aplus2, plus2, U413] > [aU312, U312] > [aU212, U212]
[tt, 0] > [aU413, aplus2, plus2, U413] > [s1, aand2, and2] > [aU212, U212]

Status:
aU113: [2,3,1]
tt: multiset
aU122: multiset
aU212: multiset
aU312: multiset
aU413: [3,2,1]
s1: [1]
aplus2: [1,2]
aand2: multiset
0: multiset
plus2: [1,2]
and2: multiset
U113: [2,3,1]
U122: multiset
U212: multiset
U312: multiset
U413: [3,2,1]

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

a__U11(tt, V1, V2) → a__U12(a__isNat(V1), V2)
a__U12(tt, V2) → a__U13(a__isNat(V2))
a__U21(tt, V1) → a__U22(a__isNat(V1))
a__U31(tt, N) → mark(N)
a__U41(tt, M, N) → s(a__plus(mark(N), mark(M)))
a__and(tt, X) → mark(X)
a__isNat(plus(V1, V2)) → a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)
a__isNatKind(plus(V1, V2)) → a__and(a__isNatKind(V1), isNatKind(V2))
a__isNatKind(s(V1)) → a__isNatKind(V1)
a__plus(N, 0) → a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__plus(N, s(M)) → a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)


(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a__U13(tt) → tt
a__U22(tt) → tt
a__isNat(0) → tt
a__isNatKind(0) → tt
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)
mark(U13(X)) → a__U13(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNatKind(X)) → a__isNatKind(X)
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)
a__U12(X1, X2) → U12(X1, X2)
a__isNat(X) → isNat(X)
a__U13(X) → U13(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__U31(X1, X2) → U31(X1, X2)
a__U41(X1, X2, X3) → U41(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNatKind(X) → isNatKind(X)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Knuth-Bendix order [KBO] with precedence:
mark1 > s1 > aU113 > aisNatKind1 > isNatKind1 > aU122 > U122 > aplus2 > plus2 > aU312 > aisNat1 > isNat1 > tt > aand2 > aU413 > and2 > 0 > aU131 > U131 > U413 > U312 > U113 > aU221 > U221 > aU212 > U212

and weight map:

tt=2
0=1
a__U13_1=1
a__U22_1=1
a__isNat_1=1
a__isNatKind_1=1
mark_1=0
isNat_1=1
U13_1=1
U22_1=1
isNatKind_1=1
s_1=1
U11_3=0
a__U11_3=0
U12_2=0
a__U12_2=0
U21_2=0
a__U21_2=0
U31_2=0
a__U31_2=0
U41_3=0
a__U41_3=0
plus_2=0
a__plus_2=0
and_2=0
a__and_2=0

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

a__U13(tt) → tt
a__U22(tt) → tt
a__isNat(0) → tt
a__isNatKind(0) → tt
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)
mark(U13(X)) → a__U13(mark(X))
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)
mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNatKind(X)) → a__isNatKind(X)
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(0) → 0
a__U11(X1, X2, X3) → U11(X1, X2, X3)
a__U12(X1, X2) → U12(X1, X2)
a__isNat(X) → isNat(X)
a__U13(X) → U13(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__U31(X1, X2) → U31(X1, X2)
a__U41(X1, X2, X3) → U41(X1, X2, X3)
a__plus(X1, X2) → plus(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNatKind(X) → isNatKind(X)


(4) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(5) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(6) YES