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(X) -> if`1(X,if`2(c,n__f(true))) (2) if`1(true,if`2(X,Y)) -> X (3) if`1(false,if`2(X,Y)) -> activate(Y) (4) f(X) -> n__f(X) (5) activate(n__f(X)) -> f(X) (6) activate(X) -> X [2] Use following polynomial interpretation: [false] = 3 rest default Remove rules with left hand side strictly bigger than right hand side: (3) [3] Use following polynomial interpretation: [activate(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (5)-(6) [4] Use following polynomial interpretation: [f(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (1), (4) [5] Use following polynomial interpretation: [if`1(x,y)] = x + y + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (2) [6] Since there are no remaining rules, termination is proved! ../tpdb/TRS/TRCSR/Ex5_Zan97_Z.trs, 0., Y Couldn't open file <60>: 60: No such file or directory