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) active(f(x)) -> mark(f(f(x))) (2) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))),x))) (3) mat(f(x),f(y)) -> f(mat(x,y)) (4) chk(no(c)) -> active(c) (5) mat(f(x),c) -> no(c) (6) f(active(x)) -> active(f(x)) (7) f(no(x)) -> no(f(x)) (8) f(mark(x)) -> mark(f(x)) (9) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))),x))) [2] Label this TRS using following interpretation that is a model: [active(x)] = 0 [f(x)] = 0 [mark(x)] = 0 [chk(x)] = 0 [no(x)] = 0 [mat(x,y)] = 0 [y] = 1 [tp(x)] = 0 rest default thus obtaining new TRS: (1a) active$0(f$1(x)) -> mark$0(f$0(f$1(x))) (1b) active$0(f$0(x)) -> mark$0(f$0(f$0(x))) (2a) chk$0(no$0(f$1(x))) -> f$0(chk$0(mat$01(f$0(f$0(f$0(f$0(f$0(f$0(f$0(f$0(f$0(f$0(X)))))))))),x))) (2b) chk$0(no$0(f$0(x))) -> f$0(chk$0(mat$00(f$0(f$0(f$0(f$0(f$0(f$0(f$0(f$0(f$0(f$0(X)))))))))),x))) (3a) mat$00(f$1(x),f$1(y)) -> f$0(mat$11(x,y)) (3b) mat$00(f$0(x),f$1(y)) -> f$0(mat$01(x,y)) (4a) chk$0(no$0(c)) -> active$0(c) (5a) mat$00(f$1(x),c) -> no$0(c) (5b) mat$00(f$0(x),c) -> no$0(c) (6a) f$0(active$1(x)) -> active$0(f$1(x)) (6b) f$0(active$0(x)) -> active$0(f$0(x)) (7a) f$0(no$1(x)) -> no$0(f$1(x)) (7b) f$0(no$0(x)) -> no$0(f$0(x)) (8a) f$0(mark$1(x)) -> mark$0(f$1(x)) (8b) f$0(mark$0(x)) -> mark$0(f$0(x)) (9a) tp$0(mark$1(x)) -> tp$0(chk$0(mat$01(f$0(f$0(f$0(f$0(f$0(f$0(f$0(f$0(f$0(f$0(X)))))))))),x))) (9b) tp$0(mark$0(x)) -> tp$0(chk$0(mat$00(f$0(f$0(f$0(f$0(f$0(f$0(f$0(f$0(f$0(f$0(X)))))))))),x))) [3] Use following polynomial interpretation: [mark$1(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (8a), (9a) [4] Use following polynomial interpretation: [no$1(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (7a) [5] Use following polynomial interpretation: [active$1(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (6a) [6] Use following polynomial interpretation: [f$1(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (2a), (3a)-(3b), (5a) [7] Unlabel this TRS to obtain the one consisting of the rules: (1)-(2), (4)-(9) [8] Label this TRS using following interpretation that is a model: [f(x)] = 1 [mat(x,y)] = 0 [tp(x)] = 0 rest default thus obtaining new TRS: (1a) active$1(f$1(x)) -> mark$1(f$1(f$1(x))) (1b) active$1(f$0(x)) -> mark$1(f$1(f$0(x))) (2a) chk$1(no$1(f$1(x))) -> f$0(chk$0(mat$11(f$1(f$1(f$1(f$1(f$1(f$1(f$1(f$1(f$1(f$0(X)))))))))),x))) (2b) chk$1(no$1(f$0(x))) -> f$0(chk$0(mat$10(f$1(f$1(f$1(f$1(f$1(f$1(f$1(f$1(f$1(f$0(X)))))))))),x))) (4a) chk$0(no$0(c)) -> active$0(c) (5a) mat$10(f$1(x),c) -> no$0(c) (5b) mat$10(f$0(x),c) -> no$0(c) (6a) f$1(active$1(x)) -> active$1(f$1(x)) (6b) f$0(active$0(x)) -> active$1(f$0(x)) (7a) f$1(no$1(x)) -> no$1(f$1(x)) (7b) f$0(no$0(x)) -> no$1(f$0(x)) (8a) f$1(mark$1(x)) -> mark$1(f$1(x)) (8b) f$0(mark$0(x)) -> mark$1(f$0(x)) (9a) tp$1(mark$1(x)) -> tp$0(chk$0(mat$11(f$1(f$1(f$1(f$1(f$1(f$1(f$1(f$1(f$1(f$0(X)))))))))),x))) (9b) tp$0(mark$0(x)) -> tp$0(chk$0(mat$10(f$1(f$1(f$1(f$1(f$1(f$1(f$1(f$1(f$1(f$0(X)))))))))),x))) [9] Use following polynomial interpretation: [tp$1(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (9a) [10] Use following polynomial interpretation: [mark$0(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (8b), (9b) [11] Unlabel this TRS to obtain the one consisting of the rules: (1)-(2), (4)-(8) [12] Use following polynomial interpretation: [chk(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (4) [13] Use following polynomial interpretation: [active(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (1) [14] Apply the Dependency Pair transformation resulting in the following dependency pairs: and 2 SCCs in the dependency graph. Proofs for those SCCs follow. [14a-1] Consider the following SCC obtained from analysis of dependency graph: (2) chk(no(f(x))) ->= f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))),x))) (5) mat(f(x),c) ->= no(c) (6) f(active(x)) ->= active(f(x)) (7) f(no(x)) ->= no(f(x)) (8) f(mark(x)) ->= mark(f(x)) (DP2) Chk(no(f(x))) -> Chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))),x)) [14a-2] Use following polynomial interpretation: [f(x)] = x + 1 [mat(x,y)] = y rest default Remove rules with left hand side strictly bigger than right hand side: (DP2) [14a-3] Since there are no remaining strict rules, relative termination is proved! [14b-1] Consider the following SCC obtained from analysis of dependency graph: (2) chk(no(f(x))) ->= f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))),x))) (5) mat(f(x),c) ->= no(c) (6) f(active(x)) ->= active(f(x)) (7) f(no(x)) ->= no(f(x)) (8) f(mark(x)) ->= mark(f(x)) (DP16) F(mark(x)) -> F(x) (DP15) F(no(x)) -> F(x) (DP14) F(active(x)) -> F(x) [14b-2] Use following polynomial interpretation: [mark(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (DP16) [14b-3] Use following polynomial interpretation: [active(x)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (DP14) [14b-4] Use following polynomial interpretation: [no(x)] = x + 1 [mat(x,y)] = x + 1 rest default Remove rules with left hand side strictly bigger than right hand side: (DP15) [14b-5] Since there are no remaining strict rules, relative termination is proved! ../tpdb/TRS/AProVE/Liveness_WRS.trs, 0.03, Y Couldn't open file <60>: 60: No such file or directory