Termination Proof using AProVE

MAYBE Termination Proof using AProVETerm Rewriting System R:
[U', U, B, A, C, X, z, y, x]
U11(tt, U', U) -> U12(equal(isNotEqualTo(U, U'), true))
U12(tt) -> false
U21(tt, B, U') -> U22(equal(isNotEqualTo(B, true), true), U')
U22(tt, U') -> U'
and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> not(xor(A, and(A, B)))
isEqualTo(U, U') -> U11(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> if_{then_{else_fi}}(isEqualTo(U, U'), false, true)
isNotEqualTo(U, U) -> false
or(A, B) -> xor(and(A, B), xor(A, B))
xor(A, A) -> false
xor(false, A) -> A
and(tt, X) -> X
equal(X, X) -> tt
if_{then_{else_fi}}(B, U, U') -> U21(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false
and(x, and(y, z)) == and(and(x, y), z)
and(x, y) == and(y, x)
or(x, or(y, z)) == or(or(x, y), z)
or(x, y) == or(y, x)
xor(x, xor(y, z)) == xor(xor(x, y), z)
xor(x, y) == xor(y, x)

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

U11'(tt, U', U) -> U12'(equal(isNotEqualTo(U, U'), true))
U11'(tt, U', U) -> EQUAL(isNotEqualTo(U, U'), true)
U11'(tt, U', U) -> ISNOTEQUALTO(U, U')
U21'(tt, B, U') -> U22'(equal(isNotEqualTo(B, true), true), U')
U21'(tt, B, U') -> EQUAL(isNotEqualTo(B, true), true)
U21'(tt, B, U') -> ISNOTEQUALTO(B, true)
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(A, xor(B, C)) -> and(A, B)
and(A, xor(B, C)) -> and(A, C)
and(and(A, A), ext) -> and(A, ext)
and(and(A, xor(B, C)), ext) -> and(xor(and(A, B), and(A, C)), ext)
and(and(A, xor(B, C)), ext) -> xor(and(A, B), and(A, C))
and(and(A, xor(B, C)), ext) -> and(A, B)
and(and(A, xor(B, C)), ext) -> and(A, C)
and(and(false, A), ext) -> and(false, ext)
IMPLIES(A, B) -> NOT(xor(A, and(A, B)))
IMPLIES(A, B) -> xor(A, and(A, B))
IMPLIES(A, B) -> and(A, B)
ISEQUALTO(U, U') -> U11'(tt, U', U)
ISNOTEQUALTO(U, U') -> IF_{THEN_{ELSE_FI}}(isEqualTo(U, U'), false, true)
ISNOTEQUALTO(U, U') -> ISEQUALTO(U, U')
or(A, B) -> xor(and(A, B), xor(A, B))
or(A, B) -> and(A, B)
or(A, B) -> xor(A, B)
or(or(A, B), ext) -> or(xor(and(A, B), xor(A, B)), ext)
or(or(A, B), ext) -> xor(and(A, B), xor(A, B))
or(or(A, B), ext) -> and(A, B)
or(or(A, B), ext) -> xor(A, B)
xor(xor(A, A), ext) -> xor(false, ext)
IF_{THEN_{ELSE_FI}}(B, U, U') -> U21'(tt, B, U')
NOT(A) -> xor(A, true)

Furthermore, R contains four SCCs.

     ↳DPs

       →DP Problem 1

         ↳Instantiation Transformation

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳AFS

Dependency Pairs:

ISEQUALTO(U, U') -> U11'(tt, U', U)
ISNOTEQUALTO(U, U') -> ISEQUALTO(U, U')
U21'(tt, B, U') -> ISNOTEQUALTO(B, true)
IF_{THEN_{ELSE_FI}}(B, U, U') -> U21'(tt, B, U')
ISNOTEQUALTO(U, U') -> IF_{THEN_{ELSE_FI}}(isEqualTo(U, U'), false, true)
U11'(tt, U', U) -> ISNOTEQUALTO(U, U')

Rules:

U11(tt, U', U) -> U12(equal(isNotEqualTo(U, U'), true))
U12(tt) -> false
U21(tt, B, U') -> U22(equal(isNotEqualTo(B, true), true), U')
U22(tt, U') -> U'
and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> not(xor(A, and(A, B)))
isEqualTo(U, U') -> U11(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> if_{then_{else_fi}}(isEqualTo(U, U'), false, true)
isNotEqualTo(U, U) -> false
or(A, B) -> xor(and(A, B), xor(A, B))
xor(A, A) -> false
xor(false, A) -> A
and(tt, X) -> X
equal(X, X) -> tt
if_{then_{else_fi}}(B, U, U') -> U21(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

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

IF_{THEN_{ELSE_FI}}(B, U, U') -> U21'(tt, B, U')

one new Dependency Pair is created:

IF_{THEN_{ELSE_FI}}(B', false, true) -> U21'(tt, B', true)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 9

             ↳Instantiation Transformation

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳AFS

Dependency Pairs:

ISNOTEQUALTO(U, U') -> ISEQUALTO(U, U')
U21'(tt, B, U') -> ISNOTEQUALTO(B, true)
IF_{THEN_{ELSE_FI}}(B', false, true) -> U21'(tt, B', true)
ISNOTEQUALTO(U, U') -> IF_{THEN_{ELSE_FI}}(isEqualTo(U, U'), false, true)
U11'(tt, U', U) -> ISNOTEQUALTO(U, U')
ISEQUALTO(U, U') -> U11'(tt, U', U)

Rules:

U11(tt, U', U) -> U12(equal(isNotEqualTo(U, U'), true))
U12(tt) -> false
U21(tt, B, U') -> U22(equal(isNotEqualTo(B, true), true), U')
U22(tt, U') -> U'
and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> not(xor(A, and(A, B)))
isEqualTo(U, U') -> U11(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> if_{then_{else_fi}}(isEqualTo(U, U'), false, true)
isNotEqualTo(U, U) -> false
or(A, B) -> xor(and(A, B), xor(A, B))
xor(A, A) -> false
xor(false, A) -> A
and(tt, X) -> X
equal(X, X) -> tt
if_{then_{else_fi}}(B, U, U') -> U21(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

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

U21'(tt, B, U') -> ISNOTEQUALTO(B, true)

one new Dependency Pair is created:

U21'(tt, B', true) -> ISNOTEQUALTO(B', true)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 9

             ↳Inst

...

               →DP Problem 10

                 ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳AFS

The following remains to be proven:
Dependency Pairs:

U21'(tt, B', true) -> ISNOTEQUALTO(B', true)
IF_{THEN_{ELSE_FI}}(B', false, true) -> U21'(tt, B', true)
ISNOTEQUALTO(U, U') -> IF_{THEN_{ELSE_FI}}(isEqualTo(U, U'), false, true)
U11'(tt, U', U) -> ISNOTEQUALTO(U, U')
ISEQUALTO(U, U') -> U11'(tt, U', U)
ISNOTEQUALTO(U, U') -> ISEQUALTO(U, U')

Rules:

U11(tt, U', U) -> U12(equal(isNotEqualTo(U, U'), true))
U12(tt) -> false
U21(tt, B, U') -> U22(equal(isNotEqualTo(B, true), true), U')
U22(tt, U') -> U'
and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> not(xor(A, and(A, B)))
isEqualTo(U, U') -> U11(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> if_{then_{else_fi}}(isEqualTo(U, U'), false, true)
isNotEqualTo(U, U) -> false
or(A, B) -> xor(and(A, B), xor(A, B))
xor(A, A) -> false
xor(false, A) -> A
and(tt, X) -> X
equal(X, X) -> tt
if_{then_{else_fi}}(B, U, U') -> U21(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Polynomial Ordering

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳AFS

Dependency Pair:

xor(xor(A, A), ext) -> xor(false, ext)

Rules:

U11(tt, U', U) -> U12(equal(isNotEqualTo(U, U'), true))
U12(tt) -> false
U21(tt, B, U') -> U22(equal(isNotEqualTo(B, true), true), U')
U22(tt, U') -> U'
and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> not(xor(A, and(A, B)))
isEqualTo(U, U') -> U11(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> if_{then_{else_fi}}(isEqualTo(U, U'), false, true)
isNotEqualTo(U, U) -> false
or(A, B) -> xor(and(A, B), xor(A, B))
xor(A, A) -> false
xor(false, A) -> A
and(tt, X) -> X
equal(X, X) -> tt
if_{then_{else_fi}}(B, U, U') -> U21(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

The following dependency pair can be strictly oriented:

xor(xor(A, A), ext) -> xor(false, ext)

Additionally, the following usable rules using the Ce-refinement can be oriented:

xor(A, A) -> false
xor(false, A) -> A

Oriented Equations:

xor(x, xor(y, z)) == xor(xor(x, y), z)
xor(x, y) == xor(y, x)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(false) = 0

POL(_xor_(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Polo

           →DP Problem 5

             ↳Dependency Graph

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳AFS

Dependency Pair:

Rules:

U11(tt, U', U) -> U12(equal(isNotEqualTo(U, U'), true))
U12(tt) -> false
U21(tt, B, U') -> U22(equal(isNotEqualTo(B, true), true), U')
U22(tt, U') -> U'
and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> not(xor(A, and(A, B)))
isEqualTo(U, U') -> U11(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> if_{then_{else_fi}}(isEqualTo(U, U'), false, true)
isNotEqualTo(U, U) -> false
or(A, B) -> xor(and(A, B), xor(A, B))
xor(A, A) -> false
xor(false, A) -> A
and(tt, X) -> X
equal(X, X) -> tt
if_{then_{else_fi}}(B, U, U') -> U21(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polynomial Ordering

       →DP Problem 4

         ↳AFS

Dependency Pairs:

and(and(false, A), ext) -> and(false, ext)
and(and(A, xor(B, C)), ext) -> and(A, C)
and(and(A, xor(B, C)), ext) -> and(A, B)
and(and(A, xor(B, C)), ext) -> and(xor(and(A, B), and(A, C)), ext)
and(and(A, A), ext) -> and(A, ext)
and(A, xor(B, C)) -> and(A, C)
and(A, xor(B, C)) -> and(A, B)

Rules:

U11(tt, U', U) -> U12(equal(isNotEqualTo(U, U'), true))
U12(tt) -> false
U21(tt, B, U') -> U22(equal(isNotEqualTo(B, true), true), U')
U22(tt, U') -> U'
and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> not(xor(A, and(A, B)))
isEqualTo(U, U') -> U11(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> if_{then_{else_fi}}(isEqualTo(U, U'), false, true)
isNotEqualTo(U, U) -> false
or(A, B) -> xor(and(A, B), xor(A, B))
xor(A, A) -> false
xor(false, A) -> A
and(tt, X) -> X
equal(X, X) -> tt
if_{then_{else_fi}}(B, U, U') -> U21(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

The following dependency pairs can be strictly oriented:

and(and(A, xor(B, C)), ext) -> and(A, C)
and(and(A, xor(B, C)), ext) -> and(A, B)
and(A, xor(B, C)) -> and(A, C)
and(A, xor(B, C)) -> and(A, B)

Additionally, the following usable rules using the Ce-refinement can be oriented:

and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
xor(A, A) -> false
xor(false, A) -> A

Oriented Equations:

and(x, and(y, z)) == and(and(x, y), z)
and(x, y) == and(y, x)
xor(x, xor(y, z)) == xor(xor(x, y), z)
xor(x, y) == xor(y, x)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(false) = 0

POL(_and_(x₁, x₂)) = x₁ + x₁·x₂ + x₂

POL(_xor_(x₁, x₂)) = 1 + x₁ + x₂

POL(true) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 6

             ↳Argument Filtering and Ordering

       →DP Problem 4

         ↳AFS

Dependency Pairs:

and(and(false, A), ext) -> and(false, ext)
and(and(A, xor(B, C)), ext) -> and(xor(and(A, B), and(A, C)), ext)
and(and(A, A), ext) -> and(A, ext)

Rules:

U11(tt, U', U) -> U12(equal(isNotEqualTo(U, U'), true))
U12(tt) -> false
U21(tt, B, U') -> U22(equal(isNotEqualTo(B, true), true), U')
U22(tt, U') -> U'
and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> not(xor(A, and(A, B)))
isEqualTo(U, U') -> U11(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> if_{then_{else_fi}}(isEqualTo(U, U'), false, true)
isNotEqualTo(U, U) -> false
or(A, B) -> xor(and(A, B), xor(A, B))
xor(A, A) -> false
xor(false, A) -> A
and(tt, X) -> X
equal(X, X) -> tt
if_{then_{else_fi}}(B, U, U') -> U21(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

The following dependency pairs can be strictly oriented:

and(and(false, A), ext) -> and(false, ext)
and(and(A, xor(B, C)), ext) -> and(xor(and(A, B), and(A, C)), ext)
and(and(A, A), ext) -> and(A, ext)

The following usable rules using the Ce-refinement can be oriented:

and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
xor(A, A) -> false
xor(false, A) -> A

Oriented Equations:

and(x, and(y, z)) == and(and(x, y), z)
and(x, y) == and(y, x)
xor(x, xor(y, z)) == xor(xor(x, y), z)
xor(x, y) == xor(y, x)

Used ordering: AC-Compatible Recursive Path Order with Status with Precedence:

and > xor > false

Status:

xor: flat
and: flat

resulting in one new DP problem.
Used Argument Filtering System:

and(x₁, x₂) -> and(x₁, x₂)
xor(x₁, x₂) -> xor(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 6

             ↳AFS

...

               →DP Problem 8

                 ↳Dependency Graph

       →DP Problem 4

         ↳AFS

Dependency Pair:

Rules:

U11(tt, U', U) -> U12(equal(isNotEqualTo(U, U'), true))
U12(tt) -> false
U21(tt, B, U') -> U22(equal(isNotEqualTo(B, true), true), U')
U22(tt, U') -> U'
and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> not(xor(A, and(A, B)))
isEqualTo(U, U') -> U11(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> if_{then_{else_fi}}(isEqualTo(U, U'), false, true)
isNotEqualTo(U, U) -> false
or(A, B) -> xor(and(A, B), xor(A, B))
xor(A, A) -> false
xor(false, A) -> A
and(tt, X) -> X
equal(X, X) -> tt
if_{then_{else_fi}}(B, U, U') -> U21(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Argument Filtering and Ordering

Dependency Pair:

or(or(A, B), ext) -> or(xor(and(A, B), xor(A, B)), ext)

Rules:

U11(tt, U', U) -> U12(equal(isNotEqualTo(U, U'), true))
U12(tt) -> false
U21(tt, B, U') -> U22(equal(isNotEqualTo(B, true), true), U')
U22(tt, U') -> U'
and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> not(xor(A, and(A, B)))
isEqualTo(U, U') -> U11(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> if_{then_{else_fi}}(isEqualTo(U, U'), false, true)
isNotEqualTo(U, U) -> false
or(A, B) -> xor(and(A, B), xor(A, B))
xor(A, A) -> false
xor(false, A) -> A
and(tt, X) -> X
equal(X, X) -> tt
if_{then_{else_fi}}(B, U, U') -> U21(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

The following dependency pair can be strictly oriented:

or(or(A, B), ext) -> or(xor(and(A, B), xor(A, B)), ext)

The following usable rules using the Ce-refinement can be oriented:

xor(A, A) -> false
xor(false, A) -> A
and(A, A) -> A
and(A, xor(B, C)) -> xor(and(A, B), and(A, C))
and(false, A) -> false
and(true, A) -> A
or(A, B) -> xor(and(A, B), xor(A, B))

Oriented Equations:

and(x, and(y, z)) == and(and(x, y), z)
and(x, y) == and(y, x)
xor(x, xor(y, z)) == xor(xor(x, y), z)
xor(x, y) == xor(y, x)
or(x, or(y, z)) == or(or(x, y), z)
or(x, y) == or(y, x)

Used ordering: AC-Compatible Recursive Path Order with Status with Precedence:

or > and > xor > false

Status:

xor: flat
and: flat
or: flat

resulting in one new DP problem.
Used Argument Filtering System:

and(x₁, x₂) -> and(x₁, x₂)
xor(x₁, x₂) -> xor(x₁, x₂)
or(x₁, x₂) -> or(x₁, x₂)

Termination of R could not be shown.
Duration:
0:19 minutes

POL(false)	= 0
POL(_xor_(x₁, x₂))	= 1 + x₁ + x₂

POL(false)	= 0
POL(_and_(x₁, x₂))	= x₁ + x₁·x₂ + x₂
POL(_xor_(x₁, x₂))	= 1 + x₁ + x₂
POL(true)	= 0