0.00/0.04 MAYBE 0.00/0.04 0.00/0.04 -- Is this system SN? ...MAYBE. 0.00/0.04 0.00/0.04 We split firstr-order part and higher-order part, and do modular checking by a general modularity. 0.00/0.04 0.00/0.04 ******** FO SN check ******** 0.00/0.04 Check SN using NaTT (Nagoya Termination Tool) 0.00/0.04 Input TRS: 0.00/0.04 1: f(X,X) -> a() 0.00/0.04 2: f(X,s(X)) -> b() 0.00/0.04 3: _(X1,X2) -> X1 0.00/0.04 4: _(X1,X2) -> X2 0.00/0.04 Number of strict rules: 4 0.00/0.04 Direct POLO(bPol) ... removes: 4 1 3 2 0.00/0.04 a w: 0 0.00/0.04 s w: x1 + 1 0.00/0.04 b w: 2 0.00/0.04 _ w: 2 * x1 + 2 * x2 + 1 0.00/0.04 f w: x1 + 2 * x2 + 1 0.00/0.04 Number of strict rules: 0 0.00/0.04 0.00/0.04 ... 0.00/0.04 Input TRS: 0.00/0.04 1: f(X,X) -> a() 0.00/0.04 2: f(X,s(X)) -> b() 0.00/0.04 3: _(X1,X2) -> X1 0.00/0.04 4: _(X1,X2) -> X2 0.00/0.04 Number of strict rules: 4 0.00/0.04 Direct POLO(bPol) ... removes: 4 1 3 2 0.00/0.04 a w: 0 0.00/0.04 s w: x1 + 1 0.00/0.04 b w: 2 0.00/0.04 _ w: 2 * x1 + 2 * x2 + 1 0.00/0.04 f w: x1 + 2 * x2 + 1 0.00/0.04 Number of strict rules: 0 0.00/0.04 >>YES 0.00/0.04 0.00/0.04 ******** Signature ******** 0.00/0.04 mu : (o -> o) -> o 0.00/0.04 ******** Computation rules ******** 0.00/0.04 (3) mu(x.Z[x]) => Z[mu(x.Z[x])] 0.00/0.04 0.00/0.04 0.00/0.04 ******** General Schema criterion ******** 0.00/0.04 Checking function dependency >>OK 0.00/0.04 Checking type dependency >>OK 0.00/0.04 Checking (1) f(X,X) => a 0.00/0.04 (fun f>a) >>True 0.00/0.04 Checking (2) f(X,s(X)) => b 0.00/0.04 (fun f>b) >>True 0.00/0.04 Checking (3) mu(x.Z[x]) => Z[mu(x.Z[x])] 0.00/0.04 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 0.00/0.04 (fun mu=mu) subterm comparison of args w. LR LR >>False 0.00/0.04 0.00/0.04 Try again using status RL 0.00/0.04 Checking (1) f(X,X) => a 0.00/0.04 (fun f>a) >>True 0.00/0.04 Checking (2) f(X,s(X)) => b 0.00/0.04 (fun f>b) >>True 0.00/0.04 Checking (3) mu(x.Z[x]) => Z[mu(x.Z[x])] 0.00/0.04 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 0.00/0.04 (fun mu=mu) subterm comparison of args w. RL RL >>False 0.00/0.04 0.00/0.04 Try again using status Mul 0.00/0.04 Checking (1) f(X,X) => a 0.00/0.04 (fun f>a) >>True 0.00/0.04 Checking (2) f(X,s(X)) => b 0.00/0.04 (fun f>b) >>True 0.00/0.04 Checking (3) mu(x.Z[x]) => Z[mu(x.Z[x])] 0.00/0.04 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 0.00/0.04 (fun mu=mu) subterm comparison of args w. Mul Mul >>False 0.00/0.04 Checking function dependency >>OK 0.00/0.04 Checking type dependency >>OK 0.00/0.04 Checking (1) f(X,X) => a 0.00/0.04 (fun f>a) >>True 0.00/0.04 Checking (2) f(X,s(X)) => b 0.00/0.04 (fun f>b) >>True 0.00/0.04 Checking (3) mu(x.Z[x]) => Z[mu(x.Z[x])] 0.00/0.04 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 0.00/0.04 (fun mu=mu) subterm comparison of args w. LR LR >>False 0.00/0.04 0.00/0.04 Try again using status RL 0.00/0.04 Checking (1) f(X,X) => a 0.00/0.04 (fun f>a) >>True 0.00/0.04 Checking (2) f(X,s(X)) => b 0.00/0.04 (fun f>b) >>True 0.00/0.04 Checking (3) mu(x.Z[x]) => Z[mu(x.Z[x])] 0.00/0.04 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 0.00/0.04 (fun mu=mu) subterm comparison of args w. RL RL >>False 0.00/0.04 0.00/0.04 Try again using status Mul 0.00/0.04 Checking (1) f(X,X) => a 0.00/0.04 (fun f>a) >>True 0.00/0.04 Checking (2) f(X,s(X)) => b 0.00/0.04 (fun f>b) >>True 0.00/0.04 Checking (3) mu(x.Z[x]) => Z[mu(x.Z[x])] 0.00/0.04 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 0.00/0.04 (fun mu=mu) subterm comparison of args w. Mul Mul >>False 0.00/0.04 Checking function dependency >>OK 0.00/0.04 Checking type dependency >>OK 0.00/0.04 Checking (3) mu(x.Z[x]) => Z[mu(x.Z[x])] 0.00/0.04 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 0.00/0.04 (fun mu=mu) subterm comparison of args w. LR LR >>False 0.00/0.04 0.00/0.04 Try again using status RL 0.00/0.04 Checking (3) mu(x.Z[x]) => Z[mu(x.Z[x])] 0.00/0.04 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 0.00/0.04 (fun mu=mu) subterm comparison of args w. RL RL >>False 0.00/0.04 0.00/0.04 Try again using status Mul 0.00/0.04 Checking (3) mu(x.Z[x]) => Z[mu(x.Z[x])] 0.00/0.04 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 0.00/0.04 (fun mu=mu) subterm comparison of args w. Mul Mul >>False 0.00/0.04 #No idea.. 0.00/0.04 ******** Critical pairs ******** 0.00/0.04 #All are joinable, but CR is not sure (Total 0 CPs) 0.00/0.04 0.00/0.04 ******** Signature ******** 0.00/0.04 f : o -> o -> o 0.00/0.04 s : o -> o 0.00/0.04 a : o 0.00/0.04 b : o 0.00/0.04 mu : (o -> o) -> o 0.00/0.04 0.00/0.04 ******** Computation rules ******** 0.00/0.04 (1) f(X,X) => a 0.00/0.04 (2) f(X,s(X)) => b 0.00/0.04 (3) mu(x.Z[x]) => Z[mu(x.Z[x])] 0.00/0.04 0.00/0.04 MAYBE 0.00/0.04 EOF