Certification Problem

Input (TPDB TRS_Standard/SK90/2.32)

The rewrite relation of the following TRS is considered.

not(x) if(x,false,true) (1)
and(x,y) if(x,y,false) (2)
or(x,y) if(x,true,y) (3)
implies(x,y) if(x,y,true) (4)
=(x,x) true (5)
=(x,y) if(x,y,not(y)) (6)
if(true,x,y) x (7)
if(false,x,y) y (8)
if(x,x,if(x,false,true)) true (9)
=(x,y) if(x,y,if(y,false,true)) (10)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[not(x1)] = 1 · x1
[if(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[false] = 0
[true] = 0
[and(x1, x2)] = 2 + 2 · x1 + 2 · x2
[or(x1, x2)] = 2 + 2 · x1 + 2 · x2
[implies(x1, x2)] = 1 + 2 · x1 + 1 · x2
[=(x1, x2)] = 1 + 2 · x1 + 2 · x2
all of the following rules can be deleted.
and(x,y) if(x,y,false) (2)
or(x,y) if(x,true,y) (3)
implies(x,y) if(x,y,true) (4)
=(x,x) true (5)
=(x,y) if(x,y,not(y)) (6)
=(x,y) if(x,y,if(y,false,true)) (10)

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(false) = 2 weight(false) = 1
prec(true) = 3 weight(true) = 1
prec(not) = 1 weight(not) = 2
prec(if) = 0 weight(if) = 0
all of the following rules can be deleted.
not(x) if(x,false,true) (1)
if(true,x,y) x (7)
if(false,x,y) y (8)
if(x,x,if(x,false,true)) true (9)

1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.