MAYBE Termination Proof using AProVETerm Rewriting System R:
[N, V1, V2, V]
U11-Thruth-os-osb-Nat-os-csb(tt, N) -> U12-os-osb-Thruth-os-csb(is'Inf-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N))))
U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb(V1, V2) -> U11-Thruth-os-osb-Nat-os-csb(V1, V2)
U12-Thruth(tt) -> tt
U21-Thruth(tt) -> tt
U21-os-osb-Thruth-os-csb(V1) -> U21-Thruth(V1)
U31-Thruth(tt) -> tt
U31-os-osb-Thruth-os-csb(V1) -> U31-Thruth(V1)
is'Inf-os-osb-Nat-os-csb(V) -> isInf-os-osb-Nat-os-csb(V)
is'Inf-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N)) -> U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb(isNat-os-osb-Nat-os-csb(N), N)
is'Nat-os-osb-Nat-os-csb(V) -> isNat-os-osb-Nat-os-csb(V)
is'Thruth-Thruth(V) -> tt
is'Thruth-os-osb-Thruth-os-csb(V1) -> is'Thruth-Thruth(V1)
isNat-os-osb-Nat-os-csb(0) -> tt
isNat-os-osb-Nat-os-csb(V) -> U21-os-osb-Thruth-os-csb(isInf-os-osb-Nat-os-csb(V))
isNat-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(V1)) -> U31-os-osb-Thruth-os-csb(isNat-os-osb-Nat-os-csb(V1))

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

ISNAT-OS-OSB-NAT-OS-CSB(V) -> U21-OS-OSB-THRUTH-OS-CSB(isInf-os-osb-Nat-os-csb(V))
ISNAT-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(V1)) -> U31-OS-OSB-THRUTH-OS-CSB(isNat-os-osb-Nat-os-csb(V1))
ISNAT-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(V1)) -> ISNAT-OS-OSB-NAT-OS-CSB(V1)
U21-OS-OSB-THRUTH-OS-CSB(V1) -> U21-THRUTH(V1)
U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(V1, V2) -> U11-THRUTH-OS-OSB-NAT-OS-CSB(V1, V2)
U11-THRUTH-OS-OSB-NAT-OS-CSB(tt, N) -> IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N)))
U31-OS-OSB-THRUTH-OS-CSB(V1) -> U31-THRUTH(V1)
IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(N)) -> U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(isNat-os-osb-Nat-os-csb(N), N)
IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(N)) -> ISNAT-OS-OSB-NAT-OS-CSB(N)
IS'NAT-OS-OSB-NAT-OS-CSB(V) -> ISNAT-OS-OSB-NAT-OS-CSB(V)
IS'THRUTH-OS-OSB-THRUTH-OS-CSB(V1) -> IS'THRUTH-THRUTH(V1)

Furthermore, R contains two SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Size-Change Principle
       →DP Problem 2
         ↳Inst


Dependency Pair:

ISNAT-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(V1)) -> ISNAT-OS-OSB-NAT-OS-CSB(V1)


Rules:


isNat-os-osb-Nat-os-csb(V) -> U21-os-osb-Thruth-os-csb(isInf-os-osb-Nat-os-csb(V))
isNat-os-osb-Nat-os-csb(0) -> tt
isNat-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(V1)) -> U31-os-osb-Thruth-os-csb(isNat-os-osb-Nat-os-csb(V1))
U21-os-osb-Thruth-os-csb(V1) -> U21-Thruth(V1)
U31-Thruth(tt) -> tt
U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb(V1, V2) -> U11-Thruth-os-osb-Nat-os-csb(V1, V2)
U11-Thruth-os-osb-Nat-os-csb(tt, N) -> U12-os-osb-Thruth-os-csb(is'Inf-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N))))
U21-Thruth(tt) -> tt
U31-os-osb-Thruth-os-csb(V1) -> U31-Thruth(V1)
is'Inf-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N)) -> U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb(isNat-os-osb-Nat-os-csb(N), N)
is'Inf-os-osb-Nat-os-csb(V) -> isInf-os-osb-Nat-os-csb(V)
U12-Thruth(tt) -> tt
is'Thruth-Thruth(V) -> tt
is'Nat-os-osb-Nat-os-csb(V) -> isNat-os-osb-Nat-os-csb(V)
is'Thruth-os-osb-Thruth-os-csb(V1) -> is'Thruth-Thruth(V1)





We number the DPs as follows:
  1. ISNAT-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(V1)) -> ISNAT-OS-OSB-NAT-OS-CSB(V1)
and get the following Size-Change Graph(s):
{1} , {1}
1>1

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
s-os-osb-Nat-os-csb(x1) -> s-os-osb-Nat-os-csb(x1)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳Instantiation Transformation


Dependency Pairs:

IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(N)) -> U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(isNat-os-osb-Nat-os-csb(N), N)
U11-THRUTH-OS-OSB-NAT-OS-CSB(tt, N) -> IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N)))
U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(V1, V2) -> U11-THRUTH-OS-OSB-NAT-OS-CSB(V1, V2)


Rules:


isNat-os-osb-Nat-os-csb(V) -> U21-os-osb-Thruth-os-csb(isInf-os-osb-Nat-os-csb(V))
isNat-os-osb-Nat-os-csb(0) -> tt
isNat-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(V1)) -> U31-os-osb-Thruth-os-csb(isNat-os-osb-Nat-os-csb(V1))
U21-os-osb-Thruth-os-csb(V1) -> U21-Thruth(V1)
U31-Thruth(tt) -> tt
U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb(V1, V2) -> U11-Thruth-os-osb-Nat-os-csb(V1, V2)
U11-Thruth-os-osb-Nat-os-csb(tt, N) -> U12-os-osb-Thruth-os-csb(is'Inf-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N))))
U21-Thruth(tt) -> tt
U31-os-osb-Thruth-os-csb(V1) -> U31-Thruth(V1)
is'Inf-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N)) -> U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb(isNat-os-osb-Nat-os-csb(N), N)
is'Inf-os-osb-Nat-os-csb(V) -> isInf-os-osb-Nat-os-csb(V)
U12-Thruth(tt) -> tt
is'Thruth-Thruth(V) -> tt
is'Nat-os-osb-Nat-os-csb(V) -> isNat-os-osb-Nat-os-csb(V)
is'Thruth-os-osb-Thruth-os-csb(V1) -> is'Thruth-Thruth(V1)





On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(N)) -> U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(isNat-os-osb-Nat-os-csb(N), N)
one new Dependency Pair is created:

IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N''))) -> U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(isNat-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N'')), s-os-osb-Nat-os-csb(N''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳Inst
           →DP Problem 3
             ↳Instantiation Transformation


Dependency Pairs:

U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(V1, V2) -> U11-THRUTH-OS-OSB-NAT-OS-CSB(V1, V2)
IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N''))) -> U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(isNat-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N'')), s-os-osb-Nat-os-csb(N''))
U11-THRUTH-OS-OSB-NAT-OS-CSB(tt, N) -> IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N)))


Rules:


isNat-os-osb-Nat-os-csb(V) -> U21-os-osb-Thruth-os-csb(isInf-os-osb-Nat-os-csb(V))
isNat-os-osb-Nat-os-csb(0) -> tt
isNat-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(V1)) -> U31-os-osb-Thruth-os-csb(isNat-os-osb-Nat-os-csb(V1))
U21-os-osb-Thruth-os-csb(V1) -> U21-Thruth(V1)
U31-Thruth(tt) -> tt
U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb(V1, V2) -> U11-Thruth-os-osb-Nat-os-csb(V1, V2)
U11-Thruth-os-osb-Nat-os-csb(tt, N) -> U12-os-osb-Thruth-os-csb(is'Inf-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N))))
U21-Thruth(tt) -> tt
U31-os-osb-Thruth-os-csb(V1) -> U31-Thruth(V1)
is'Inf-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N)) -> U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb(isNat-os-osb-Nat-os-csb(N), N)
is'Inf-os-osb-Nat-os-csb(V) -> isInf-os-osb-Nat-os-csb(V)
U12-Thruth(tt) -> tt
is'Thruth-Thruth(V) -> tt
is'Nat-os-osb-Nat-os-csb(V) -> isNat-os-osb-Nat-os-csb(V)
is'Thruth-os-osb-Thruth-os-csb(V1) -> is'Thruth-Thruth(V1)





On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(V1, V2) -> U11-THRUTH-OS-OSB-NAT-OS-CSB(V1, V2)
one new Dependency Pair is created:

U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(V1', s-os-osb-Nat-os-csb(N'''')) -> U11-THRUTH-OS-OSB-NAT-OS-CSB(V1', s-os-osb-Nat-os-csb(N''''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳Inst
           →DP Problem 3
             ↳Inst
             ...
               →DP Problem 4
                 ↳Instantiation Transformation





Dependency Pairs:
U11-THRUTH-OS-OSB-NAT-OS-CSB(tt, N) -> IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N)))
U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(V1', s-os-osb-Nat-os-csb(N'''')) -> U11-THRUTH-OS-OSB-NAT-OS-CSB(V1', s-os-osb-Nat-os-csb(N''''))
IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N''))) -> U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(isNat-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N'')), s-os-osb-Nat-os-csb(N''))

Rules:

isNat-os-osb-Nat-os-csb(V) -> U21-os-osb-Thruth-os-csb(isInf-os-osb-Nat-os-csb(V))

isNat-os-osb-Nat-os-csb(0) -> tt

isNat-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(V1)) -> U31-os-osb-Thruth-os-csb(isNat-os-osb-Nat-os-csb(V1))

U21-os-osb-Thruth-os-csb(V1) -> U21-Thruth(V1)

U31-Thruth(tt) -> tt

U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb(V1, V2) -> U11-Thruth-os-osb-Nat-os-csb(V1, V2)

U11-Thruth-os-osb-Nat-os-csb(tt, N) -> U12-os-osb-Thruth-os-csb(is'Inf-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N))))

U21-Thruth(tt) -> tt

U31-os-osb-Thruth-os-csb(V1) -> U31-Thruth(V1)

is'Inf-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N)) -> U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb(isNat-os-osb-Nat-os-csb(N), N)

is'Inf-os-osb-Nat-os-csb(V) -> isInf-os-osb-Nat-os-csb(V)

U12-Thruth(tt) -> tt

is'Thruth-Thruth(V) -> tt

is'Nat-os-osb-Nat-os-csb(V) -> isNat-os-osb-Nat-os-csb(V)

is'Thruth-os-osb-Thruth-os-csb(V1) -> is'Thruth-Thruth(V1)




On this DP problem, an Instantiation SCC transformation can be performed.

As a result of transforming the rule 


U11-THRUTH-OS-OSB-NAT-OS-CSB(tt, N) -> IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N)))
one new Dependency Pair
is created:


U11-THRUTH-OS-OSB-NAT-OS-CSB(tt, s-os-osb-Nat-os-csb(N'''''')) -> IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N''''''))))

The transformation is resulting in one new DP problem:




   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳Inst
           →DP Problem 3
             ↳Inst
             ...
               →DP Problem 5
                 ↳Remaining Obligation(s)







The following remains to be proven:
Dependency Pairs:
IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N''))) -> U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(isNat-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N'')), s-os-osb-Nat-os-csb(N''))
U11-THRUTH-OS-OSB-NAT-OS-CSB(tt, s-os-osb-Nat-os-csb(N'''''')) -> IS'INF-OS-OSB-NAT-OS-CSB(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N''''''))))
U11-OS-OSB-THRUTH-OS-CSB-OS-OSB-NAT-OS-CSB(V1', s-os-osb-Nat-os-csb(N'''')) -> U11-THRUTH-OS-OSB-NAT-OS-CSB(V1', s-os-osb-Nat-os-csb(N''''))

Rules:

isNat-os-osb-Nat-os-csb(V) -> U21-os-osb-Thruth-os-csb(isInf-os-osb-Nat-os-csb(V))

isNat-os-osb-Nat-os-csb(0) -> tt

isNat-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(V1)) -> U31-os-osb-Thruth-os-csb(isNat-os-osb-Nat-os-csb(V1))

U21-os-osb-Thruth-os-csb(V1) -> U21-Thruth(V1)

U31-Thruth(tt) -> tt

U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb(V1, V2) -> U11-Thruth-os-osb-Nat-os-csb(V1, V2)

U11-Thruth-os-osb-Nat-os-csb(tt, N) -> U12-os-osb-Thruth-os-csb(is'Inf-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N))))

U21-Thruth(tt) -> tt

U31-os-osb-Thruth-os-csb(V1) -> U31-Thruth(V1)

is'Inf-os-osb-Nat-os-csb(s-os-osb-Nat-os-csb(N)) -> U11-os-osb-Thruth-os-csb-os-osb-Nat-os-csb(isNat-os-osb-Nat-os-csb(N), N)

is'Inf-os-osb-Nat-os-csb(V) -> isInf-os-osb-Nat-os-csb(V)

U12-Thruth(tt) -> tt

is'Thruth-Thruth(V) -> tt

is'Nat-os-osb-Nat-os-csb(V) -> isNat-os-osb-Nat-os-csb(V)

is'Thruth-os-osb-Thruth-os-csb(V1) -> is'Thruth-Thruth(V1)



The Proof could not be continued due to a Timeout.

Termination of R could not be shown.

Duration: 
10:00 minutes