YES (VAR t n x a b c) (RULES g(A) -> A g(B) -> A g(B) -> B g(C) -> A g(C) -> B g(C) -> C foldB(t,0) -> t foldB(t,s(n)) -> f(foldB(t,n),B) foldC(t,0) -> t foldC(t,s(n)) -> f(foldC(t,n),C) f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),C) -> triple(a,b,s(c)) f'(triple(a,b,c),B) -> f(triple(a,b,c),A) f'(triple(a,b,c),A) -> f''(foldB(triple(s(a),0,c),b)) f''(triple(a,b,c)) -> foldC(triple(a,b,0),c) fold(t,x,0) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) ) Proving termination of rewriting for filliatre3: -> Dependency pairs: nF_foldB(t,s(n)) -> nF_f(foldB(t,n),B) nF_foldB(t,s(n)) -> nF_foldB(t,n) nF_foldC(t,s(n)) -> nF_f(foldC(t,n),C) nF_foldC(t,s(n)) -> nF_foldC(t,n) nF_f(t,x) -> nF_f'(t,g(x)) nF_f(t,x) -> nF_g(x) nF_f'(triple(a,b,c),B) -> nF_f(triple(a,b,c),A) nF_f'(triple(a,b,c),A) -> nF_f''(foldB(triple(s(a),0,c),b)) nF_f'(triple(a,b,c),A) -> nF_foldB(triple(s(a),0,c),b) nF_f''(triple(a,b,c)) -> nF_foldC(triple(a,b,0),c) nF_fold(t,x,s(n)) -> nF_f(fold(t,x,n),x) nF_fold(t,x,s(n)) -> nF_fold(t,x,n) -> Proof of termination for filliatre3_1_1: -> -> Dependency pairs in cycle: nF_fold(t,x,s(n)) -> nF_fold(t,x,n) Termination proved: Cycles verify subterm criterion. -> Proof of termination for filliatre3_1_2: -> -> Dependency pairs in cycle: nF_foldB(t,s(n)) -> nF_f(foldB(t,n),B) nF_f'(triple(a,b,c),A) -> nF_foldB(triple(s(a),0,c),b) nF_f(t,x) -> nF_f'(t,g(x)) nF_f'(triple(a,b,c),B) -> nF_f(triple(a,b,c),A) nF_foldC(t,s(n)) -> nF_f(foldC(t,n),C) nF_f''(triple(a,b,c)) -> nF_foldC(triple(a,b,0),c) nF_f'(triple(a,b,c),A) -> nF_f''(foldB(triple(s(a),0,c),b)) nF_foldC(t,s(n)) -> nF_foldC(t,n) nF_foldB(t,s(n)) -> nF_foldB(t,n) UsableRules: g(A) -> A g(B) -> A g(B) -> B g(C) -> A g(C) -> B g(C) -> C foldB(t,0) -> t foldB(t,s(n)) -> f(foldB(t,n),B) foldC(t,0) -> t foldC(t,s(n)) -> f(foldC(t,n),C) f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),C) -> triple(a,b,s(c)) f'(triple(a,b,c),B) -> f(triple(a,b,c),A) f'(triple(a,b,c),A) -> f''(foldB(triple(s(a),0,c),b)) f''(triple(a,b,c)) -> foldC(triple(a,b,0),c) Polynomial Interpretation: [g](X) = 0 [A] = 0 [B] = 0 [C] = 0 [foldB](X1,X2) = X1 [0] = 0 [s](X) = X + 1 [f](X1,X2) = X1 [foldC](X1,X2) = X1 [f'](X1,X2) = X1 [triple](X1,X2,X3) = X2 [f''](X) = X [fold](X1,X2,X3) = 0 [nF_foldB](X1,X2) = X1 + X2 [nF_f'](X1,X2) = X1 [nF_f](X1,X2) = X1 [nF_foldC](X1,X2) = X1 [nF_f''](X) = X TIME: 7.3426e-2 -> -> Dependency pairs in cycle: nF_foldB(t,s(n)) -> nF_f(foldB(t,n),B) nF_f'(triple(a,b,c),A) -> nF_foldB(triple(s(a),0,c),b) nF_f(t,x) -> nF_f'(t,g(x)) nF_foldC(t,s(n)) -> nF_f(foldC(t,n),C) nF_foldC(t,s(n)) -> nF_foldC(t,n) nF_f''(triple(a,b,c)) -> nF_foldC(triple(a,b,0),c) nF_f'(triple(a,b,c),A) -> nF_f''(foldB(triple(s(a),0,c),b)) nF_f'(triple(a,b,c),B) -> nF_f(triple(a,b,c),A) UsableRules: g(A) -> A g(B) -> A g(B) -> B g(C) -> A g(C) -> B g(C) -> C foldB(t,0) -> t foldB(t,s(n)) -> f(foldB(t,n),B) foldC(t,0) -> t foldC(t,s(n)) -> f(foldC(t,n),C) f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),C) -> triple(a,b,s(c)) f'(triple(a,b,c),B) -> f(triple(a,b,c),A) f'(triple(a,b,c),A) -> f''(foldB(triple(s(a),0,c),b)) f''(triple(a,b,c)) -> foldC(triple(a,b,0),c) Polynomial Interpretation: [g](X) = X [A] = 0 [B] = 1 [C] = 1 [foldB](X1,X2) = X1 + X2 [0] = 0 [s](X) = X + 1 [f](X1,X2) = X1 + 1 [foldC](X1,X2) = X1 + X2 [f'](X1,X2) = X1 + 1 [triple](X1,X2,X3) = X2 + X3 [f''](X) = X [fold](X1,X2,X3) = 0 [nF_foldB](X1,X2) = X1 + X2 [nF_f'](X1,X2) = X1 + X2 [nF_f](X1,X2) = X1 + X2 [nF_foldC](X1,X2) = X1 + X2 [nF_f''](X) = X TIME: 8.216e-2 -> -> Dependency pairs in cycle: nF_foldB(t,s(n)) -> nF_f(foldB(t,n),B) nF_f'(triple(a,b,c),A) -> nF_foldB(triple(s(a),0,c),b) nF_f(t,x) -> nF_f'(t,g(x)) nF_foldC(t,s(n)) -> nF_f(foldC(t,n),C) nF_f''(triple(a,b,c)) -> nF_foldC(triple(a,b,0),c) nF_f'(triple(a,b,c),A) -> nF_f''(foldB(triple(s(a),0,c),b)) nF_foldC(t,s(n)) -> nF_foldC(t,n) UsableRules: g(A) -> A g(B) -> A g(B) -> B g(C) -> A g(C) -> B g(C) -> C foldB(t,0) -> t foldB(t,s(n)) -> f(foldB(t,n),B) foldC(t,0) -> t foldC(t,s(n)) -> f(foldC(t,n),C) f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),C) -> triple(a,b,s(c)) f'(triple(a,b,c),B) -> f(triple(a,b,c),A) f'(triple(a,b,c),A) -> f''(foldB(triple(s(a),0,c),b)) f''(triple(a,b,c)) -> foldC(triple(a,b,0),c) Polynomial Interpretation: [g](X) = 1 [A] = 1 [B] = 1 [C] = 1 [foldB](X1,X2) = X1 + X2 [0] = 0 [s](X) = X + 1 [f](X1,X2) = X1 + 1 [foldC](X1,X2) = X1 + X2 [f'](X1,X2) = X1 + X2 [triple](X1,X2,X3) = X1 + X2 + X3 [f''](X) = X [fold](X1,X2,X3) = 0 [nF_foldB](X1,X2) = X1 + X2 [nF_f'](X1,X2) = X1 + X2 [nF_f](X1,X2) = X1 + 1 [nF_foldC](X1,X2) = X1 + X2 [nF_f''](X) = X TIME: 6.898700000000002e-2 -> -> Dependency pairs in cycle: nF_foldB(t,s(n)) -> nF_f(foldB(t,n),B) nF_f'(triple(a,b,c),A) -> nF_foldB(triple(s(a),0,c),b) nF_f(t,x) -> nF_f'(t,g(x)) nF_foldC(t,s(n)) -> nF_f(foldC(t,n),C) nF_f''(triple(a,b,c)) -> nF_foldC(triple(a,b,0),c) nF_f'(triple(a,b,c),A) -> nF_f''(foldB(triple(s(a),0,c),b)) UsableRules: g(A) -> A g(B) -> A g(B) -> B g(C) -> A g(C) -> B g(C) -> C foldB(t,0) -> t foldB(t,s(n)) -> f(foldB(t,n),B) foldC(t,0) -> t foldC(t,s(n)) -> f(foldC(t,n),C) f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),C) -> triple(a,b,s(c)) f'(triple(a,b,c),B) -> f(triple(a,b,c),A) f'(triple(a,b,c),A) -> f''(foldB(triple(s(a),0,c),b)) f''(triple(a,b,c)) -> foldC(triple(a,b,0),c) Polynomial Interpretation: [g](X) = X [A] = 1 [B] = 1 [C] = 1 [foldB](X1,X2) = X1 + X2 [0] = 0 [s](X) = X + 1 [f](X1,X2) = X1 + 1 [foldC](X1,X2) = X1 + X2 [f'](X1,X2) = X1 + 1 [triple](X1,X2,X3) = X2 + X3 [f''](X) = X [fold](X1,X2,X3) = 0 [nF_foldB](X1,X2) = X1 + X2 [nF_f'](X1,X2) = X1 + X2 [nF_f](X1,X2) = X1 + X2 [nF_foldC](X1,X2) = X1 + X2 [nF_f''](X) = X TIME: 6.7306e-2 -> -> Dependency pairs in cycle: nF_foldB(t,s(n)) -> nF_f(foldB(t,n),B) nF_f'(triple(a,b,c),A) -> nF_foldB(triple(s(a),0,c),b) nF_f(t,x) -> nF_f'(t,g(x)) UsableRules: g(A) -> A g(B) -> A g(B) -> B g(C) -> A g(C) -> B g(C) -> C foldB(t,0) -> t foldB(t,s(n)) -> f(foldB(t,n),B) foldC(t,0) -> t foldC(t,s(n)) -> f(foldC(t,n),C) f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),C) -> triple(a,b,s(c)) f'(triple(a,b,c),B) -> f(triple(a,b,c),A) f'(triple(a,b,c),A) -> f''(foldB(triple(s(a),0,c),b)) f''(triple(a,b,c)) -> foldC(triple(a,b,0),c) Polynomial Interpretation: [g](X) = 0 [A] = 0 [B] = 0 [C] = 0 [foldB](X1,X2) = X1 [0] = 0 [s](X) = 1 [f](X1,X2) = X1 [foldC](X1,X2) = X1 [f'](X1,X2) = X1 [triple](X1,X2,X3) = X2 [f''](X) = X [fold](X1,X2,X3) = 0 [nF_foldB](X1,X2) = X1 + X2 [nF_f'](X1,X2) = X1 [nF_f](X1,X2) = X1 + 1 TIME: 5.9878e-2 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.