The rewrite relation of the following TRS is considered.
a__f(a,b,X) | → | a__f(mark(X),X,mark(X)) | (1) |
a__c | → | a | (2) |
a__c | → | b | (3) |
mark(f(X1,X2,X3)) | → | a__f(mark(X1),X2,mark(X3)) | (4) |
mark(c) | → | a__c | (5) |
mark(a) | → | a | (6) |
mark(b) | → | b | (7) |
a__f(X1,X2,X3) | → | f(X1,X2,X3) | (8) |
a__c | → | c | (9) |
a__f#(a,b,X) | → | a__f#(mark(X),X,mark(X)) | (10) |
a__f#(a,b,X) | → | mark#(X) | (11) |
mark#(f(X1,X2,X3)) | → | a__f#(mark(X1),X2,mark(X3)) | (12) |
mark#(f(X1,X2,X3)) | → | mark#(X1) | (13) |
mark#(f(X1,X2,X3)) | → | mark#(X3) | (14) |
mark#(c) | → | a__c# | (15) |
mark#(c) | → | a__c# | (15) |
mark#(f(X1,X2,X3)) | → | a__f#(mark(X1),X2,mark(X3)) | (12) |
a__f#(a,b,X) | → | mark#(X) | (11) |
mark#(f(X1,X2,X3)) | → | mark#(X1) | (13) |
mark#(f(X1,X2,X3)) | → | mark#(X3) | (14) |
t0 | = | a__f#(mark(mark(a__c)),mark(a__c),mark(mark(a__c))) |
→R | a__f#(mark(mark(a__c)),mark(a__c),mark(mark(c))) | |
→R | a__f#(mark(mark(a__c)),mark(a__c),mark(a__c)) | |
→R | a__f#(mark(mark(a__c)),mark(a__c),mark(c)) | |
→R | a__f#(mark(mark(a__c)),mark(a__c),a__c) | |
→R | a__f#(mark(mark(a__c)),mark(b),a__c) | |
→R | a__f#(mark(mark(a__c)),b,a__c) | |
→R | a__f#(mark(mark(a)),b,a__c) | |
→R | a__f#(mark(a),b,a__c) | |
→R | a__f#(a,b,a__c) | |
→P | a__f#(mark(a__c),a__c,mark(a__c)) | |
→R | a__f#(mark(a__c),b,mark(a__c)) | |
→R | a__f#(mark(a),b,mark(a__c)) | |
→R | a__f#(a,b,mark(a__c)) | |
→P | a__f#(mark(mark(a__c)),mark(a__c),mark(mark(a__c))) | |
= | t14 |