YES TPA v.1.0 Result: TRS is terminating Default interpretations for symbols are not printed. For polynomial interpretations and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans) defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols. [1] TRS loaded from input file: (1) f(f(X)) -> f(a(b(f(X)))) (2) f(a(g(X))) -> b(X) (3) b(X) -> a(X) [2] Use following polynomial interpretation: [g(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (2) [3] Label this TRS using following interpretation that is a model: [f(x)] = 1 [a(x)] = 0 [b(x)] = 0 rest default thus obtaining new TRS: (1a) f$1(f$1(X)) -> f$0(a$0(b$1(f$1(X)))) (1b) f$1(f$0(X)) -> f$0(a$0(b$1(f$0(X)))) (3a) b$1(X) -> a$1(X) (3b) b$0(X) -> a$0(X) [4] Use following polynomial interpretation: [b$0(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (3b) [5] Use following polynomial interpretation: [f$1(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (1a)-(1b) [6] Use following polynomial interpretation: [b$1(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (3a) [7] Since there are no remaining rules, termination is proved! ../tpdb/TRS/Rubio/p266.trs, 0., Y Couldn't open file <60>: 60: No such file or directory