The rewrite relation of the following TRS is considered.
| app(app(lt,app(s,x)),app(s,y)) | → | app(app(lt,x),y) | (1) |
| app(app(lt,0),app(s,y)) | → | true | (2) |
| app(app(lt,y),0) | → | false | (3) |
| app(app(eq,x),x) | → | true | (4) |
| app(app(eq,app(s,x)),0) | → | false | (5) |
| app(app(eq,0),app(s,x)) | → | false | (6) |
| app(app(member,w),null) | → | false | (7) |
| app(app(member,w),app(app(app(fork,x),y),z)) | → | app(app(app(if,app(app(lt,w),y)),app(app(member,w),x)),app(app(app(if,app(app(eq,w),y)),true),app(app(member,w),z))) | (8) |
| app#(app(lt,app(s,x)),app(s,y)) | → | app#(lt,x) | (9) |
| app#(app(lt,app(s,x)),app(s,y)) | → | app#(app(lt,x),y) | (10) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(app(member,w),z) | (11) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(eq,w) | (12) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(app(eq,w),y) | (13) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(if,app(app(eq,w),y)) | (14) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(app(if,app(app(eq,w),y)),true) | (15) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(app(app(if,app(app(eq,w),y)),true),app(app(member,w),z)) | (16) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(app(member,w),x) | (17) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(lt,w) | (18) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(app(lt,w),y) | (19) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(if,app(app(lt,w),y)) | (20) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(app(if,app(app(lt,w),y)),app(app(member,w),x)) | (21) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(app(app(if,app(app(lt,w),y)),app(app(member,w),x)),app(app(app(if,app(app(eq,w),y)),true),app(app(member,w),z))) | (22) |
The dependency pairs are split into 2 components.
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(app(member,w),z) | (11) |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(app(member,w),x) | (17) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(app(member,w),z) | (11) |
| 2 | > | 2 | |
| 1 | ≥ | 1 | |
| app#(app(member,w),app(app(app(fork,x),y),z)) | → | app#(app(member,w),x) | (17) |
| 2 | > | 2 | |
| 1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| app#(app(lt,app(s,x)),app(s,y)) | → | app#(app(lt,x),y) | (10) |
| π(app#) | = | 2 |
| app#(app(lt,app(s,x)),app(s,y)) | → | app#(app(lt,x),y) | (10) |
There are no pairs anymore.