MAYBE
Termination Proof using AProVETerm Rewriting System R:
[V, N, V1]
U101(tt) -> tt
U11(tt, V) -> isInf-osb-os-osb-Nat-os-csb-csb(V)
U111(tt) -> tt
U121(tt) -> tt
U131(tt) -> tt
U21(tt, N) -> U22(isNat-osb-os-osb-Nat-os-csb-csb(N), N)
U22(tt, N) -> U23(is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N))))
U23(tt) -> tt
U31(tt, V) -> isNat-osb-os-osb-Nat-os-csb-csb(V)
U41(tt) -> tt
U51(tt, V) -> U52(isInf-osb-os-osb-Nat-os-csb-csb(V))
U52(tt) -> tt
U61(tt, V1) -> U62(isNat-osb-os-osb-Nat-os-csb-csb(V1))
U62(tt) -> tt
U71(tt) -> tt
U81(tt) -> tt
U91(tt) -> tt
is'Inf-osb-os-osb-Nat-os-csb-csb(V) -> U11(isos-osb-Nat-os-csb(V), V)
is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)) -> U21(isos-osb-Nat-os-csb(N), N)
is'Nat-osb-os-osb-Nat-os-csb-csb(V) -> U31(isos-osb-Nat-os-csb(V), V)
is'Thruth(V) -> isThruth(V)
is'Thruth-osb-os-osb-Thruth-os-csb-csb(V) -> U41(isThruth(V))
is'os-osb-Nat-os-csb(V) -> isos-osb-Nat-os-csb(V)
is'os-osb-Thruth-os-csb(V) -> isos-osb-Thruth-os-csb(V)
isNat-osb-os-osb-Nat-os-csb-csb(0) -> tt
isNat-osb-os-osb-Nat-os-csb-csb(V) -> U51(isos-osb-Nat-os-csb(V), V)
isNat-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U61(isos-osb-Nat-os-csb(V1), V1)
isThruth(tt) -> tt
isos-osb-Nat-os-csb(0) -> tt
isos-osb-Nat-os-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U71(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(V) -> U81(is'Thruth(V))
isos-osb-Thruth-os-csb(tt) -> tt
isos-osb-Thruth-os-csb(is'Inf-osb-os-osb-Nat-os-csb-csb(V1)) -> U91(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(is'Nat-osb-os-osb-Nat-os-csb-csb(V1)) -> U101(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(is'Thruth-osb-os-osb-Thruth-os-csb-csb(V1)) -> U111(isos-osb-Thruth-os-csb(V1))
isos-osb-Thruth-os-csb(isInf-osb-os-osb-Nat-os-csb-csb(V1)) -> U121(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isNat-osb-os-osb-Nat-os-csb-csb(V1)) -> U131(isos-osb-Nat-os-csb(V1))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
IS'THRUTH-OSB-OS-OSB-THRUTH-OS-CSB-CSB(V) -> U41'(isThruth(V))
IS'THRUTH-OSB-OS-OSB-THRUTH-OS-CSB-CSB(V) -> ISTHRUTH(V)
IS'OS-OSB-NAT-OS-CSB(V) -> ISOS-OSB-NAT-OS-CSB(V)
ISOS-OSB-NAT-OS-CSB(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U71'(isos-osb-Nat-os-csb(V1))
ISOS-OSB-NAT-OS-CSB(s-osb-os-osb-Nat-os-csb-csb(V1)) -> ISOS-OSB-NAT-OS-CSB(V1)
ISNAT-OSB-OS-OSB-NAT-OS-CSB-CSB(V) -> U51'(isos-osb-Nat-os-csb(V), V)
ISNAT-OSB-OS-OSB-NAT-OS-CSB-CSB(V) -> ISOS-OSB-NAT-OS-CSB(V)
ISNAT-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U61'(isos-osb-Nat-os-csb(V1), V1)
ISNAT-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(V1)) -> ISOS-OSB-NAT-OS-CSB(V1)
U51'(tt, V) -> U52'(isInf-osb-os-osb-Nat-os-csb-csb(V))
ISOS-OSB-THRUTH-OS-CSB(is'Inf-osb-os-osb-Nat-os-csb-csb(V1)) -> U91'(isos-osb-Nat-os-csb(V1))
ISOS-OSB-THRUTH-OS-CSB(is'Inf-osb-os-osb-Nat-os-csb-csb(V1)) -> ISOS-OSB-NAT-OS-CSB(V1)
ISOS-OSB-THRUTH-OS-CSB(isNat-osb-os-osb-Nat-os-csb-csb(V1)) -> U131'(isos-osb-Nat-os-csb(V1))
ISOS-OSB-THRUTH-OS-CSB(isNat-osb-os-osb-Nat-os-csb-csb(V1)) -> ISOS-OSB-NAT-OS-CSB(V1)
ISOS-OSB-THRUTH-OS-CSB(isInf-osb-os-osb-Nat-os-csb-csb(V1)) -> U121'(isos-osb-Nat-os-csb(V1))
ISOS-OSB-THRUTH-OS-CSB(isInf-osb-os-osb-Nat-os-csb-csb(V1)) -> ISOS-OSB-NAT-OS-CSB(V1)
ISOS-OSB-THRUTH-OS-CSB(V) -> U81'(is'Thruth(V))
ISOS-OSB-THRUTH-OS-CSB(V) -> IS'THRUTH(V)
ISOS-OSB-THRUTH-OS-CSB(is'Nat-osb-os-osb-Nat-os-csb-csb(V1)) -> U101'(isos-osb-Nat-os-csb(V1))
ISOS-OSB-THRUTH-OS-CSB(is'Nat-osb-os-osb-Nat-os-csb-csb(V1)) -> ISOS-OSB-NAT-OS-CSB(V1)
ISOS-OSB-THRUTH-OS-CSB(is'Thruth-osb-os-osb-Thruth-os-csb-csb(V1)) -> U111'(isos-osb-Thruth-os-csb(V1))
ISOS-OSB-THRUTH-OS-CSB(is'Thruth-osb-os-osb-Thruth-os-csb-csb(V1)) -> ISOS-OSB-THRUTH-OS-CSB(V1)
IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(V) -> U11'(isos-osb-Nat-os-csb(V), V)
IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(V) -> ISOS-OSB-NAT-OS-CSB(V)
IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(N)) -> U21'(isos-osb-Nat-os-csb(N), N)
IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(N)) -> ISOS-OSB-NAT-OS-CSB(N)
U61'(tt, V1) -> U62'(isNat-osb-os-osb-Nat-os-csb-csb(V1))
U61'(tt, V1) -> ISNAT-OSB-OS-OSB-NAT-OS-CSB-CSB(V1)
IS'OS-OSB-THRUTH-OS-CSB(V) -> ISOS-OSB-THRUTH-OS-CSB(V)
IS'THRUTH(V) -> ISTHRUTH(V)
IS'NAT-OSB-OS-OSB-NAT-OS-CSB-CSB(V) -> U31'(isos-osb-Nat-os-csb(V), V)
IS'NAT-OSB-OS-OSB-NAT-OS-CSB-CSB(V) -> ISOS-OSB-NAT-OS-CSB(V)
U31'(tt, V) -> ISNAT-OSB-OS-OSB-NAT-OS-CSB-CSB(V)
U21'(tt, N) -> U22'(isNat-osb-os-osb-Nat-os-csb-csb(N), N)
U21'(tt, N) -> ISNAT-OSB-OS-OSB-NAT-OS-CSB-CSB(N)
U22'(tt, N) -> U23'(is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N))))
U22'(tt, N) -> IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)))
Furthermore, R contains four SCCs.
R
↳DPs
→DP Problem 1
↳Size-Change Principle
→DP Problem 2
↳SCP
→DP Problem 3
↳SCP
→DP Problem 4
↳Inst
Dependency Pair:
ISOS-OSB-NAT-OS-CSB(s-osb-os-osb-Nat-os-csb-csb(V1)) -> ISOS-OSB-NAT-OS-CSB(V1)
Rules:
is'Thruth-osb-os-osb-Thruth-os-csb-csb(V) -> U41(isThruth(V))
U41(tt) -> tt
isThruth(tt) -> tt
is'os-osb-Nat-os-csb(V) -> isos-osb-Nat-os-csb(V)
isos-osb-Nat-os-csb(0) -> tt
isos-osb-Nat-os-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U71(isos-osb-Nat-os-csb(V1))
isNat-osb-os-osb-Nat-os-csb-csb(V) -> U51(isos-osb-Nat-os-csb(V), V)
isNat-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U61(isos-osb-Nat-os-csb(V1), V1)
isNat-osb-os-osb-Nat-os-csb-csb(0) -> tt
U51(tt, V) -> U52(isInf-osb-os-osb-Nat-os-csb-csb(V))
isos-osb-Thruth-os-csb(tt) -> tt
isos-osb-Thruth-os-csb(is'Inf-osb-os-osb-Nat-os-csb-csb(V1)) -> U91(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isNat-osb-os-osb-Nat-os-csb-csb(V1)) -> U131(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isInf-osb-os-osb-Nat-os-csb-csb(V1)) -> U121(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(V) -> U81(is'Thruth(V))
isos-osb-Thruth-os-csb(is'Nat-osb-os-osb-Nat-os-csb-csb(V1)) -> U101(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(is'Thruth-osb-os-osb-Thruth-os-csb-csb(V1)) -> U111(isos-osb-Thruth-os-csb(V1))
U131(tt) -> tt
is'Inf-osb-os-osb-Nat-os-csb-csb(V) -> U11(isos-osb-Nat-os-csb(V), V)
is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)) -> U21(isos-osb-Nat-os-csb(N), N)
U91(tt) -> tt
U61(tt, V1) -> U62(isNat-osb-os-osb-Nat-os-csb-csb(V1))
U52(tt) -> tt
U121(tt) -> tt
is'os-osb-Thruth-os-csb(V) -> isos-osb-Thruth-os-csb(V)
U23(tt) -> tt
U71(tt) -> tt
U111(tt) -> tt
is'Thruth(V) -> isThruth(V)
is'Nat-osb-os-osb-Nat-os-csb-csb(V) -> U31(isos-osb-Nat-os-csb(V), V)
U31(tt, V) -> isNat-osb-os-osb-Nat-os-csb-csb(V)
U62(tt) -> tt
U101(tt) -> tt
U11(tt, V) -> isInf-osb-os-osb-Nat-os-csb-csb(V)
U81(tt) -> tt
U21(tt, N) -> U22(isNat-osb-os-osb-Nat-os-csb-csb(N), N)
U22(tt, N) -> U23(is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N))))
We number the DPs as follows:
- ISOS-OSB-NAT-OS-CSB(s-osb-os-osb-Nat-os-csb-csb(V1)) -> ISOS-OSB-NAT-OS-CSB(V1)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
s-osb-os-osb-Nat-os-csb-csb(x1) -> s-osb-os-osb-Nat-os-csb-csb(x1)
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Size-Change Principle
→DP Problem 3
↳SCP
→DP Problem 4
↳Inst
Dependency Pairs:
U61'(tt, V1) -> ISNAT-OSB-OS-OSB-NAT-OS-CSB-CSB(V1)
ISNAT-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U61'(isos-osb-Nat-os-csb(V1), V1)
Rules:
is'Thruth-osb-os-osb-Thruth-os-csb-csb(V) -> U41(isThruth(V))
U41(tt) -> tt
isThruth(tt) -> tt
is'os-osb-Nat-os-csb(V) -> isos-osb-Nat-os-csb(V)
isos-osb-Nat-os-csb(0) -> tt
isos-osb-Nat-os-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U71(isos-osb-Nat-os-csb(V1))
isNat-osb-os-osb-Nat-os-csb-csb(V) -> U51(isos-osb-Nat-os-csb(V), V)
isNat-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U61(isos-osb-Nat-os-csb(V1), V1)
isNat-osb-os-osb-Nat-os-csb-csb(0) -> tt
U51(tt, V) -> U52(isInf-osb-os-osb-Nat-os-csb-csb(V))
isos-osb-Thruth-os-csb(tt) -> tt
isos-osb-Thruth-os-csb(is'Inf-osb-os-osb-Nat-os-csb-csb(V1)) -> U91(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isNat-osb-os-osb-Nat-os-csb-csb(V1)) -> U131(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isInf-osb-os-osb-Nat-os-csb-csb(V1)) -> U121(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(V) -> U81(is'Thruth(V))
isos-osb-Thruth-os-csb(is'Nat-osb-os-osb-Nat-os-csb-csb(V1)) -> U101(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(is'Thruth-osb-os-osb-Thruth-os-csb-csb(V1)) -> U111(isos-osb-Thruth-os-csb(V1))
U131(tt) -> tt
is'Inf-osb-os-osb-Nat-os-csb-csb(V) -> U11(isos-osb-Nat-os-csb(V), V)
is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)) -> U21(isos-osb-Nat-os-csb(N), N)
U91(tt) -> tt
U61(tt, V1) -> U62(isNat-osb-os-osb-Nat-os-csb-csb(V1))
U52(tt) -> tt
U121(tt) -> tt
is'os-osb-Thruth-os-csb(V) -> isos-osb-Thruth-os-csb(V)
U23(tt) -> tt
U71(tt) -> tt
U111(tt) -> tt
is'Thruth(V) -> isThruth(V)
is'Nat-osb-os-osb-Nat-os-csb-csb(V) -> U31(isos-osb-Nat-os-csb(V), V)
U31(tt, V) -> isNat-osb-os-osb-Nat-os-csb-csb(V)
U62(tt) -> tt
U101(tt) -> tt
U11(tt, V) -> isInf-osb-os-osb-Nat-os-csb-csb(V)
U81(tt) -> tt
U21(tt, N) -> U22(isNat-osb-os-osb-Nat-os-csb-csb(N), N)
U22(tt, N) -> U23(is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N))))
We number the DPs as follows:
- U61'(tt, V1) -> ISNAT-OSB-OS-OSB-NAT-OS-CSB-CSB(V1)
- ISNAT-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U61'(isos-osb-Nat-os-csb(V1), V1)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
s-osb-os-osb-Nat-os-csb-csb(x1) -> s-osb-os-osb-Nat-os-csb-csb(x1)
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳SCP
→DP Problem 3
↳Size-Change Principle
→DP Problem 4
↳Inst
Dependency Pair:
ISOS-OSB-THRUTH-OS-CSB(is'Thruth-osb-os-osb-Thruth-os-csb-csb(V1)) -> ISOS-OSB-THRUTH-OS-CSB(V1)
Rules:
is'Thruth-osb-os-osb-Thruth-os-csb-csb(V) -> U41(isThruth(V))
U41(tt) -> tt
isThruth(tt) -> tt
is'os-osb-Nat-os-csb(V) -> isos-osb-Nat-os-csb(V)
isos-osb-Nat-os-csb(0) -> tt
isos-osb-Nat-os-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U71(isos-osb-Nat-os-csb(V1))
isNat-osb-os-osb-Nat-os-csb-csb(V) -> U51(isos-osb-Nat-os-csb(V), V)
isNat-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U61(isos-osb-Nat-os-csb(V1), V1)
isNat-osb-os-osb-Nat-os-csb-csb(0) -> tt
U51(tt, V) -> U52(isInf-osb-os-osb-Nat-os-csb-csb(V))
isos-osb-Thruth-os-csb(tt) -> tt
isos-osb-Thruth-os-csb(is'Inf-osb-os-osb-Nat-os-csb-csb(V1)) -> U91(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isNat-osb-os-osb-Nat-os-csb-csb(V1)) -> U131(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isInf-osb-os-osb-Nat-os-csb-csb(V1)) -> U121(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(V) -> U81(is'Thruth(V))
isos-osb-Thruth-os-csb(is'Nat-osb-os-osb-Nat-os-csb-csb(V1)) -> U101(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(is'Thruth-osb-os-osb-Thruth-os-csb-csb(V1)) -> U111(isos-osb-Thruth-os-csb(V1))
U131(tt) -> tt
is'Inf-osb-os-osb-Nat-os-csb-csb(V) -> U11(isos-osb-Nat-os-csb(V), V)
is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)) -> U21(isos-osb-Nat-os-csb(N), N)
U91(tt) -> tt
U61(tt, V1) -> U62(isNat-osb-os-osb-Nat-os-csb-csb(V1))
U52(tt) -> tt
U121(tt) -> tt
is'os-osb-Thruth-os-csb(V) -> isos-osb-Thruth-os-csb(V)
U23(tt) -> tt
U71(tt) -> tt
U111(tt) -> tt
is'Thruth(V) -> isThruth(V)
is'Nat-osb-os-osb-Nat-os-csb-csb(V) -> U31(isos-osb-Nat-os-csb(V), V)
U31(tt, V) -> isNat-osb-os-osb-Nat-os-csb-csb(V)
U62(tt) -> tt
U101(tt) -> tt
U11(tt, V) -> isInf-osb-os-osb-Nat-os-csb-csb(V)
U81(tt) -> tt
U21(tt, N) -> U22(isNat-osb-os-osb-Nat-os-csb-csb(N), N)
U22(tt, N) -> U23(is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N))))
We number the DPs as follows:
- ISOS-OSB-THRUTH-OS-CSB(is'Thruth-osb-os-osb-Thruth-os-csb-csb(V1)) -> ISOS-OSB-THRUTH-OS-CSB(V1)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
is'Thruth-osb-os-osb-Thruth-os-csb-csb(x1) -> is'Thruth-osb-os-osb-Thruth-os-csb-csb(x1)
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳SCP
→DP Problem 3
↳SCP
→DP Problem 4
↳Instantiation Transformation
Dependency Pairs:
U22'(tt, N) -> IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)))
U21'(tt, N) -> U22'(isNat-osb-os-osb-Nat-os-csb-csb(N), N)
IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(N)) -> U21'(isos-osb-Nat-os-csb(N), N)
Rules:
is'Thruth-osb-os-osb-Thruth-os-csb-csb(V) -> U41(isThruth(V))
U41(tt) -> tt
isThruth(tt) -> tt
is'os-osb-Nat-os-csb(V) -> isos-osb-Nat-os-csb(V)
isos-osb-Nat-os-csb(0) -> tt
isos-osb-Nat-os-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U71(isos-osb-Nat-os-csb(V1))
isNat-osb-os-osb-Nat-os-csb-csb(V) -> U51(isos-osb-Nat-os-csb(V), V)
isNat-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U61(isos-osb-Nat-os-csb(V1), V1)
isNat-osb-os-osb-Nat-os-csb-csb(0) -> tt
U51(tt, V) -> U52(isInf-osb-os-osb-Nat-os-csb-csb(V))
isos-osb-Thruth-os-csb(tt) -> tt
isos-osb-Thruth-os-csb(is'Inf-osb-os-osb-Nat-os-csb-csb(V1)) -> U91(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isNat-osb-os-osb-Nat-os-csb-csb(V1)) -> U131(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isInf-osb-os-osb-Nat-os-csb-csb(V1)) -> U121(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(V) -> U81(is'Thruth(V))
isos-osb-Thruth-os-csb(is'Nat-osb-os-osb-Nat-os-csb-csb(V1)) -> U101(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(is'Thruth-osb-os-osb-Thruth-os-csb-csb(V1)) -> U111(isos-osb-Thruth-os-csb(V1))
U131(tt) -> tt
is'Inf-osb-os-osb-Nat-os-csb-csb(V) -> U11(isos-osb-Nat-os-csb(V), V)
is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)) -> U21(isos-osb-Nat-os-csb(N), N)
U91(tt) -> tt
U61(tt, V1) -> U62(isNat-osb-os-osb-Nat-os-csb-csb(V1))
U52(tt) -> tt
U121(tt) -> tt
is'os-osb-Thruth-os-csb(V) -> isos-osb-Thruth-os-csb(V)
U23(tt) -> tt
U71(tt) -> tt
U111(tt) -> tt
is'Thruth(V) -> isThruth(V)
is'Nat-osb-os-osb-Nat-os-csb-csb(V) -> U31(isos-osb-Nat-os-csb(V), V)
U31(tt, V) -> isNat-osb-os-osb-Nat-os-csb-csb(V)
U62(tt) -> tt
U101(tt) -> tt
U11(tt, V) -> isInf-osb-os-osb-Nat-os-csb-csb(V)
U81(tt) -> tt
U21(tt, N) -> U22(isNat-osb-os-osb-Nat-os-csb-csb(N), N)
U22(tt, N) -> U23(is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N))))
On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule
IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(N)) -> U21'(isos-osb-Nat-os-csb(N), N)
one new Dependency Pair
is created:
IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N''))) -> U21'(isos-osb-Nat-os-csb(s-osb-os-osb-Nat-os-csb-csb(N'')), s-osb-os-osb-Nat-os-csb-csb(N''))
The transformation is resulting in one new DP problem:
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳SCP
→DP Problem 3
↳SCP
→DP Problem 4
↳Inst
→DP Problem 5
↳Instantiation Transformation
Dependency Pairs:
U21'(tt, N) -> U22'(isNat-osb-os-osb-Nat-os-csb-csb(N), N)
IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N''))) -> U21'(isos-osb-Nat-os-csb(s-osb-os-osb-Nat-os-csb-csb(N'')), s-osb-os-osb-Nat-os-csb-csb(N''))
U22'(tt, N) -> IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)))
Rules:
is'Thruth-osb-os-osb-Thruth-os-csb-csb(V) -> U41(isThruth(V))
U41(tt) -> tt
isThruth(tt) -> tt
is'os-osb-Nat-os-csb(V) -> isos-osb-Nat-os-csb(V)
isos-osb-Nat-os-csb(0) -> tt
isos-osb-Nat-os-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U71(isos-osb-Nat-os-csb(V1))
isNat-osb-os-osb-Nat-os-csb-csb(V) -> U51(isos-osb-Nat-os-csb(V), V)
isNat-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U61(isos-osb-Nat-os-csb(V1), V1)
isNat-osb-os-osb-Nat-os-csb-csb(0) -> tt
U51(tt, V) -> U52(isInf-osb-os-osb-Nat-os-csb-csb(V))
isos-osb-Thruth-os-csb(tt) -> tt
isos-osb-Thruth-os-csb(is'Inf-osb-os-osb-Nat-os-csb-csb(V1)) -> U91(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isNat-osb-os-osb-Nat-os-csb-csb(V1)) -> U131(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isInf-osb-os-osb-Nat-os-csb-csb(V1)) -> U121(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(V) -> U81(is'Thruth(V))
isos-osb-Thruth-os-csb(is'Nat-osb-os-osb-Nat-os-csb-csb(V1)) -> U101(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(is'Thruth-osb-os-osb-Thruth-os-csb-csb(V1)) -> U111(isos-osb-Thruth-os-csb(V1))
U131(tt) -> tt
is'Inf-osb-os-osb-Nat-os-csb-csb(V) -> U11(isos-osb-Nat-os-csb(V), V)
is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)) -> U21(isos-osb-Nat-os-csb(N), N)
U91(tt) -> tt
U61(tt, V1) -> U62(isNat-osb-os-osb-Nat-os-csb-csb(V1))
U52(tt) -> tt
U121(tt) -> tt
is'os-osb-Thruth-os-csb(V) -> isos-osb-Thruth-os-csb(V)
U23(tt) -> tt
U71(tt) -> tt
U111(tt) -> tt
is'Thruth(V) -> isThruth(V)
is'Nat-osb-os-osb-Nat-os-csb-csb(V) -> U31(isos-osb-Nat-os-csb(V), V)
U31(tt, V) -> isNat-osb-os-osb-Nat-os-csb-csb(V)
U62(tt) -> tt
U101(tt) -> tt
U11(tt, V) -> isInf-osb-os-osb-Nat-os-csb-csb(V)
U81(tt) -> tt
U21(tt, N) -> U22(isNat-osb-os-osb-Nat-os-csb-csb(N), N)
U22(tt, N) -> U23(is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N))))
On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule
U21'(tt, N) -> U22'(isNat-osb-os-osb-Nat-os-csb-csb(N), N)
one new Dependency Pair
is created:
U21'(tt, s-osb-os-osb-Nat-os-csb-csb(N'''')) -> U22'(isNat-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N'''')), s-osb-os-osb-Nat-os-csb-csb(N''''))
The transformation is resulting in one new DP problem:
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳SCP
→DP Problem 3
↳SCP
→DP Problem 4
↳Inst
→DP Problem 5
↳Inst
... →DP Problem 6
↳Instantiation Transformation
Dependency Pairs:
U22'(tt, N) -> IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)))
U21'(tt, s-osb-os-osb-Nat-os-csb-csb(N'''')) -> U22'(isNat-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N'''')), s-osb-os-osb-Nat-os-csb-csb(N''''))
IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N''))) -> U21'(isos-osb-Nat-os-csb(s-osb-os-osb-Nat-os-csb-csb(N'')), s-osb-os-osb-Nat-os-csb-csb(N''))
Rules:
is'Thruth-osb-os-osb-Thruth-os-csb-csb(V) -> U41(isThruth(V))
U41(tt) -> tt
isThruth(tt) -> tt
is'os-osb-Nat-os-csb(V) -> isos-osb-Nat-os-csb(V)
isos-osb-Nat-os-csb(0) -> tt
isos-osb-Nat-os-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U71(isos-osb-Nat-os-csb(V1))
isNat-osb-os-osb-Nat-os-csb-csb(V) -> U51(isos-osb-Nat-os-csb(V), V)
isNat-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U61(isos-osb-Nat-os-csb(V1), V1)
isNat-osb-os-osb-Nat-os-csb-csb(0) -> tt
U51(tt, V) -> U52(isInf-osb-os-osb-Nat-os-csb-csb(V))
isos-osb-Thruth-os-csb(tt) -> tt
isos-osb-Thruth-os-csb(is'Inf-osb-os-osb-Nat-os-csb-csb(V1)) -> U91(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isNat-osb-os-osb-Nat-os-csb-csb(V1)) -> U131(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isInf-osb-os-osb-Nat-os-csb-csb(V1)) -> U121(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(V) -> U81(is'Thruth(V))
isos-osb-Thruth-os-csb(is'Nat-osb-os-osb-Nat-os-csb-csb(V1)) -> U101(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(is'Thruth-osb-os-osb-Thruth-os-csb-csb(V1)) -> U111(isos-osb-Thruth-os-csb(V1))
U131(tt) -> tt
is'Inf-osb-os-osb-Nat-os-csb-csb(V) -> U11(isos-osb-Nat-os-csb(V), V)
is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)) -> U21(isos-osb-Nat-os-csb(N), N)
U91(tt) -> tt
U61(tt, V1) -> U62(isNat-osb-os-osb-Nat-os-csb-csb(V1))
U52(tt) -> tt
U121(tt) -> tt
is'os-osb-Thruth-os-csb(V) -> isos-osb-Thruth-os-csb(V)
U23(tt) -> tt
U71(tt) -> tt
U111(tt) -> tt
is'Thruth(V) -> isThruth(V)
is'Nat-osb-os-osb-Nat-os-csb-csb(V) -> U31(isos-osb-Nat-os-csb(V), V)
U31(tt, V) -> isNat-osb-os-osb-Nat-os-csb-csb(V)
U62(tt) -> tt
U101(tt) -> tt
U11(tt, V) -> isInf-osb-os-osb-Nat-os-csb-csb(V)
U81(tt) -> tt
U21(tt, N) -> U22(isNat-osb-os-osb-Nat-os-csb-csb(N), N)
U22(tt, N) -> U23(is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N))))
On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule
U22'(tt, N) -> IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)))
one new Dependency Pair
is created:
U22'(tt, s-osb-os-osb-Nat-os-csb-csb(N'''''')) -> IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N''''''))))
The transformation is resulting in one new DP problem:
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳SCP
→DP Problem 3
↳SCP
→DP Problem 4
↳Inst
→DP Problem 5
↳Inst
... →DP Problem 7
↳Remaining Obligation(s)
The following remains to be proven:
Dependency Pairs:
IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N''))) -> U21'(isos-osb-Nat-os-csb(s-osb-os-osb-Nat-os-csb-csb(N'')), s-osb-os-osb-Nat-os-csb-csb(N''))
U22'(tt, s-osb-os-osb-Nat-os-csb-csb(N'''''')) -> IS'INF-OSB-OS-OSB-NAT-OS-CSB-CSB(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N''''''))))
U21'(tt, s-osb-os-osb-Nat-os-csb-csb(N'''')) -> U22'(isNat-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N'''')), s-osb-os-osb-Nat-os-csb-csb(N''''))
Rules:
is'Thruth-osb-os-osb-Thruth-os-csb-csb(V) -> U41(isThruth(V))
U41(tt) -> tt
isThruth(tt) -> tt
is'os-osb-Nat-os-csb(V) -> isos-osb-Nat-os-csb(V)
isos-osb-Nat-os-csb(0) -> tt
isos-osb-Nat-os-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U71(isos-osb-Nat-os-csb(V1))
isNat-osb-os-osb-Nat-os-csb-csb(V) -> U51(isos-osb-Nat-os-csb(V), V)
isNat-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(V1)) -> U61(isos-osb-Nat-os-csb(V1), V1)
isNat-osb-os-osb-Nat-os-csb-csb(0) -> tt
U51(tt, V) -> U52(isInf-osb-os-osb-Nat-os-csb-csb(V))
isos-osb-Thruth-os-csb(tt) -> tt
isos-osb-Thruth-os-csb(is'Inf-osb-os-osb-Nat-os-csb-csb(V1)) -> U91(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isNat-osb-os-osb-Nat-os-csb-csb(V1)) -> U131(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(isInf-osb-os-osb-Nat-os-csb-csb(V1)) -> U121(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(V) -> U81(is'Thruth(V))
isos-osb-Thruth-os-csb(is'Nat-osb-os-osb-Nat-os-csb-csb(V1)) -> U101(isos-osb-Nat-os-csb(V1))
isos-osb-Thruth-os-csb(is'Thruth-osb-os-osb-Thruth-os-csb-csb(V1)) -> U111(isos-osb-Thruth-os-csb(V1))
U131(tt) -> tt
is'Inf-osb-os-osb-Nat-os-csb-csb(V) -> U11(isos-osb-Nat-os-csb(V), V)
is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N)) -> U21(isos-osb-Nat-os-csb(N), N)
U91(tt) -> tt
U61(tt, V1) -> U62(isNat-osb-os-osb-Nat-os-csb-csb(V1))
U52(tt) -> tt
U121(tt) -> tt
is'os-osb-Thruth-os-csb(V) -> isos-osb-Thruth-os-csb(V)
U23(tt) -> tt
U71(tt) -> tt
U111(tt) -> tt
is'Thruth(V) -> isThruth(V)
is'Nat-osb-os-osb-Nat-os-csb-csb(V) -> U31(isos-osb-Nat-os-csb(V), V)
U31(tt, V) -> isNat-osb-os-osb-Nat-os-csb-csb(V)
U62(tt) -> tt
U101(tt) -> tt
U11(tt, V) -> isInf-osb-os-osb-Nat-os-csb-csb(V)
U81(tt) -> tt
U21(tt, N) -> U22(isNat-osb-os-osb-Nat-os-csb-csb(N), N)
U22(tt, N) -> U23(is'Inf-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(s-osb-os-osb-Nat-os-csb-csb(N))))
The Proof could not be continued due to a Timeout.
Termination of R could not be shown.
Duration:
10:00 minutes