(VAR V1 V2 N M)
(STRATEGY CONTEXTSENSITIVE 
  (U11 1)
  (tt)
  (U12 1)
  (isNatKind)
  (U13 1)
  (U14 1)
  (U15 1)
  (isNat)
  (U16 1)
  (U21 1)
  (U22 1)
  (U23 1)
  (U31 1)
  (U32 1)
  (U41 1)
  (U51 1)
  (U52 1)
  (U61 1)
  (U62 1)
  (U63 1)
  (U64 1)
  (s 1)
  (plus 1 2)
  (0)
)
(RULES 
U11(tt,V1,V2) -> U12(isNatKind(V1),V1,V2)
U12(tt,V1,V2) -> U13(isNatKind(V2),V1,V2)
U13(tt,V1,V2) -> U14(isNatKind(V2),V1,V2)
U14(tt,V1,V2) -> U15(isNat(V1),V2)
U15(tt,V2) -> U16(isNat(V2))
U16(tt) -> tt
U21(tt,V1) -> U22(isNatKind(V1),V1)
U22(tt,V1) -> U23(isNat(V1))
U23(tt) -> tt
U31(tt,V2) -> U32(isNatKind(V2))
U32(tt) -> tt
U41(tt) -> tt
U51(tt,N) -> U52(isNatKind(N),N)
U52(tt,N) -> N
U61(tt,M,N) -> U62(isNatKind(M),M,N)
U62(tt,M,N) -> U63(isNat(N),M,N)
U63(tt,M,N) -> U64(isNatKind(N),M,N)
U64(tt,M,N) -> s(plus(N,M))
isNat(0) -> tt
isNat(plus(V1,V2)) -> U11(isNatKind(V1),V1,V2)
isNat(s(V1)) -> U21(isNatKind(V1),V1)
isNatKind(0) -> tt
isNatKind(plus(V1,V2)) -> U31(isNatKind(V1),V2)
isNatKind(s(V1)) -> U41(isNatKind(V1))
plus(N,0) -> U51(isNat(N),N)
plus(N,s(M)) -> U61(isNat(M),M,N)
)

Proving termination of context-sensitive rewriting for MYNAT_complete_noand:

-> Dependency pairs:
nF_U11(tt,V1,V2) -> nF_U12(isNatKind(V1),V1,V2)
nF_U11(tt,V1,V2) -> nF_isNatKind(V1)
nF_U12(tt,V1,V2) -> nF_U13(isNatKind(V2),V1,V2)
nF_U12(tt,V1,V2) -> nF_isNatKind(V2)
nF_U13(tt,V1,V2) -> nF_U14(isNatKind(V2),V1,V2)
nF_U13(tt,V1,V2) -> nF_isNatKind(V2)
nF_U14(tt,V1,V2) -> nF_U15(isNat(V1),V2)
nF_U14(tt,V1,V2) -> nF_isNat(V1)
nF_U15(tt,V2) -> nF_U16(isNat(V2))
nF_U15(tt,V2) -> nF_isNat(V2)
nF_U21(tt,V1) -> nF_U22(isNatKind(V1),V1)
nF_U21(tt,V1) -> nF_isNatKind(V1)
nF_U22(tt,V1) -> nF_U23(isNat(V1))
nF_U22(tt,V1) -> nF_isNat(V1)
nF_U31(tt,V2) -> nF_U32(isNatKind(V2))
nF_U31(tt,V2) -> nF_isNatKind(V2)
nF_U51(tt,N) -> nF_U52(isNatKind(N),N)
nF_U51(tt,N) -> nF_isNatKind(N)
nF_U52(tt,N) -> N
nF_U61(tt,M,N) -> nF_U62(isNatKind(M),M,N)
nF_U61(tt,M,N) -> nF_isNatKind(M)
nF_U62(tt,M,N) -> nF_U63(isNat(N),M,N)
nF_U62(tt,M,N) -> nF_isNat(N)
nF_U63(tt,M,N) -> nF_U64(isNatKind(N),M,N)
nF_U63(tt,M,N) -> nF_isNatKind(N)
nF_U64(tt,M,N) -> nF_plus(N,M)
nF_U64(tt,M,N) -> N
nF_U64(tt,M,N) -> M
nF_isNat(plus(V1,V2)) -> nF_U11(isNatKind(V1),V1,V2)
nF_isNat(plus(V1,V2)) -> nF_isNatKind(V1)
nF_isNat(s(V1)) -> nF_U21(isNatKind(V1),V1)
nF_isNat(s(V1)) -> nF_isNatKind(V1)
nF_isNatKind(plus(V1,V2)) -> nF_U31(isNatKind(V1),V2)
nF_isNatKind(plus(V1,V2)) -> nF_isNatKind(V1)
nF_isNatKind(s(V1)) -> nF_U41(isNatKind(V1))
nF_isNatKind(s(V1)) -> nF_isNatKind(V1)
nF_plus(N,0) -> nF_U51(isNat(N),N)
nF_plus(N,0) -> nF_isNat(N)
nF_plus(N,s(M)) -> nF_U61(isNat(M),M,N)
nF_plus(N,s(M)) -> nF_isNat(M)

-> Proof of termination for MYNAT_complete_noand_1_1:
-> -> Dependency pairs in cycle:
nF_U61(tt,M,N) -> nF_U62(isNatKind(M),M,N)
nF_plus(N,s(M)) -> nF_U61(isNat(M),M,N)
nF_U64(tt,M,N) -> nF_plus(N,M)
nF_U63(tt,M,N) -> nF_U64(isNatKind(N),M,N)
nF_U62(tt,M,N) -> nF_U63(isNat(N),M,N)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for MYNAT_complete_noand_1_2:
-> -> Dependency pairs in cycle:
nF_U11(tt,V1,V2) -> nF_U12(isNatKind(V1),V1,V2)
nF_isNat(plus(V1,V2)) -> nF_U11(isNatKind(V1),V1,V2)
nF_U22(tt,V1) -> nF_isNat(V1)
nF_U21(tt,V1) -> nF_U22(isNatKind(V1),V1)
nF_isNat(s(V1)) -> nF_U21(isNatKind(V1),V1)
nF_U15(tt,V2) -> nF_isNat(V2)
nF_U14(tt,V1,V2) -> nF_U15(isNat(V1),V2)
nF_U13(tt,V1,V2) -> nF_U14(isNatKind(V2),V1,V2)
nF_U12(tt,V1,V2) -> nF_U13(isNatKind(V2),V1,V2)
nF_U14(tt,V1,V2) -> nF_isNat(V1)

Usable Rules:
U11(tt,V1,V2) -> U12(isNatKind(V1),V1,V2)
U12(tt,V1,V2) -> U13(isNatKind(V2),V1,V2)
U13(tt,V1,V2) -> U14(isNatKind(V2),V1,V2)
U14(tt,V1,V2) -> U15(isNat(V1),V2)
U15(tt,V2) -> U16(isNat(V2))
U16(tt) -> tt
U21(tt,V1) -> U22(isNatKind(V1),V1)
U22(tt,V1) -> U23(isNat(V1))
U23(tt) -> tt
U31(tt,V2) -> U32(isNatKind(V2))
U32(tt) -> tt
U41(tt) -> tt
isNat(0) -> tt
isNat(plus(V1,V2)) -> U11(isNatKind(V1),V1,V2)
isNat(s(V1)) -> U21(isNatKind(V1),V1)
isNatKind(0) -> tt
isNatKind(plus(V1,V2)) -> U31(isNatKind(V1),V2)
isNatKind(s(V1)) -> U41(isNatKind(V1))

Polynomial Interpretation:

[U11](X1,X2,X3) = 0
[tt] = 0
[U12](X1,X2,X3) = 0
[isNatKind](X) = X
[U13](X1,X2,X3) = 0
[U14](X1,X2,X3) = 0
[U15](X1,X2) = 0
[isNat](X) = X
[U16](X) = 0
[U21](X1,X2) = 0
[U22](X1,X2) = 0
[U23](X) = 0
[U31](X1,X2) = 0
[U32](X) = 0
[U41](X) = 0
[U51](X1,X2) = 0
[U52](X1,X2) = 0
[U61](X1,X2,X3) = 0
[U62](X1,X2,X3) = 0
[U63](X1,X2,X3) = 0
[U64](X1,X2,X3) = 0
[s](X) = X
[plus](X1,X2) = X1 + X2 + 1
[0] = 1
[nF_U11](X1,X2,X3) = X2 + X3 + 1
[nF_isNat](X) = X
[nF_U22](X1,X2) = X2
[nF_U21](X1,X2) = X2
[nF_U15](X1,X2) = X2
[nF_U14](X1,X2,X3) = X2 + X3 + 1
[nF_U13](X1,X2,X3) = X2 + X3 + 1
[nF_U12](X1,X2,X3) = X2 + X3 + 1

TIME: 5.924600000000002e-2

-> -> Dependency pairs in cycle:
nF_U11(tt,V1,V2) -> nF_U12(isNatKind(V1),V1,V2)
nF_isNat(plus(V1,V2)) -> nF_U11(isNatKind(V1),V1,V2)
nF_U15(tt,V2) -> nF_isNat(V2)
nF_U14(tt,V1,V2) -> nF_U15(isNat(V1),V2)
nF_U13(tt,V1,V2) -> nF_U14(isNatKind(V2),V1,V2)
nF_U12(tt,V1,V2) -> nF_U13(isNatKind(V2),V1,V2)
nF_U22(tt,V1) -> nF_isNat(V1)
nF_U21(tt,V1) -> nF_U22(isNatKind(V1),V1)
nF_isNat(s(V1)) -> nF_U21(isNatKind(V1),V1)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for MYNAT_complete_noand_1_3:
-> -> Dependency pairs in cycle:
nF_isNatKind(s(V1)) -> nF_isNatKind(V1)
nF_isNatKind(plus(V1,V2)) -> nF_isNatKind(V1)
nF_U31(tt,V2) -> nF_isNatKind(V2)
nF_isNatKind(plus(V1,V2)) -> nF_U31(isNatKind(V1),V2)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in CSDG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.