YES (VAR x y w z) (RULES app(app(lt,app(s,x)),app(s,y)) -> app(app(lt,x),y) app(app(lt,0),app(s,y)) -> true app(app(lt,y),0) -> false app(app(eq,x),x) -> true app(app(eq,app(s,x)),0) -> false app(app(eq,0),app(s,x)) -> false app(app(member,w),null) -> false 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))) ) The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting. Proving termination of innermost rewriting for BTreeMember: -> Dependency pairs: nF_app(app(lt,app(s,x)),app(s,y)) -> nF_app(app(lt,x),y) nF_app(app(lt,app(s,x)),app(s,y)) -> nF_app(lt,x) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_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))) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(if,app(app(lt,w),y)),app(app(member,w),x)) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(if,app(app(lt,w),y)) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(lt,w),y) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(lt,w) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(member,w),x) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(member,w) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(app(if,app(app(eq,w),y)),true),app(app(member,w),z)) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(if,app(app(eq,w),y)),true) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(if,app(app(eq,w),y)) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(eq,w),y) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(eq,w) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(member,w),z) -> Dependency pairs narrowed: nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(eq,w),y) -> New dependency pairs: There are no new dependency pairs. -> Proof of termination for BTreeMember_1: -> -> Dependency pairs in cycle: nF_app(app(lt,app(s,x)),app(s,y)) -> nF_app(app(lt,x),y) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(app(if,app(app(eq,w),y)),true),app(app(member,w),z)) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(member,w),z) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(member,w),x) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(lt,w),y) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(if,app(app(lt,w),y)),app(app(member,w),x)) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_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))) UsableRules: app(app(lt,app(s,x)),app(s,y)) -> app(app(lt,x),y) app(app(lt,0),app(s,y)) -> true app(app(lt,y),0) -> false app(app(eq,x),x) -> true app(app(eq,app(s,x)),0) -> false app(app(eq,0),app(s,x)) -> false app(app(member,w),null) -> false 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))) Polynomial Interpretation: [app](X1,X2) = X1 [lt] = 0 [s] = 0 [0] = 0 [true] = 0 [false] = 0 [eq] = 0 [member] = 1 [null] = 0 [fork] = 0 [if] = 0 [nF_app](X1,X2) = X1 TIME: 7.9312e-2 -> -> Dependency pairs in cycle: nF_app(app(lt,app(s,x)),app(s,y)) -> nF_app(app(lt,x),y) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(if,app(app(lt,w),y)),app(app(member,w),x)) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(lt,w),y) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(member,w),x) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(member,w),z) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(app(if,app(app(eq,w),y)),true),app(app(member,w),z)) UsableRules: app(app(lt,app(s,x)),app(s,y)) -> app(app(lt,x),y) app(app(lt,0),app(s,y)) -> true app(app(lt,y),0) -> false app(app(eq,x),x) -> true app(app(eq,app(s,x)),0) -> false app(app(eq,0),app(s,x)) -> false app(app(member,w),null) -> false 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))) Polynomial Interpretation: [app](X1,X2) = X1 [lt] = 0 [s] = 0 [0] = 0 [true] = 0 [false] = 0 [eq] = 0 [member] = 1 [null] = 0 [fork] = 0 [if] = 0 [nF_app](X1,X2) = X1 TIME: 6.6345e-2 -> -> Dependency pairs in cycle: nF_app(app(lt,app(s,x)),app(s,y)) -> nF_app(app(lt,x),y) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(member,w),z) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(member,w),x) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(lt,w),y) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(if,app(app(lt,w),y)),app(app(member,w),x)) UsableRules: app(app(lt,app(s,x)),app(s,y)) -> app(app(lt,x),y) app(app(lt,0),app(s,y)) -> true app(app(lt,y),0) -> false app(app(eq,x),x) -> true app(app(eq,app(s,x)),0) -> false app(app(eq,0),app(s,x)) -> false app(app(member,w),null) -> false 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))) Polynomial Interpretation: [app](X1,X2) = X1 [lt] = 0 [s] = 0 [0] = 0 [true] = 0 [false] = 0 [eq] = 0 [member] = 1 [null] = 0 [fork] = 0 [if] = 0 [nF_app](X1,X2) = X1 TIME: 6.2645e-2 -> -> Dependency pairs in cycle: nF_app(app(lt,app(s,x)),app(s,y)) -> nF_app(app(lt,x),y) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(lt,w),y) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(member,w),x) nF_app(app(member,w),app(app(app(fork,x),y),z)) -> nF_app(app(member,w),z) Termination proved: Cycles verify subterm criterion. SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in DG + base ordering Upper bound for coeffs: 1 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Linear Coeffs in polynomials: No rationals Delta: automatic Termination was proved succesfully.