0.002/0.002 NO 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S M:S N:S V1:S V2:S X:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U13 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U33 1) 0.002/0.002 (U41 1) 0.002/0.002 (U51 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (and 1) 0.002/0.002 (isNat) 0.002/0.002 (isNatKind) 0.002/0.002 (plus 1 2) 0.002/0.002 (x 1 2) 0.002/0.002 (0) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (s 1) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U11(tt,V1:S,V2:S) -> U12(isNat(V1:S),V2:S) 0.002/0.002 U12(tt,V2:S) -> U13(isNat(V2:S)) 0.002/0.002 U13(tt) -> tt 0.002/0.002 U21(tt,V1:S) -> U22(isNat(V1:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt,V1:S,V2:S) -> U32(isNat(V1:S),V2:S) 0.002/0.002 U32(tt,V2:S) -> U33(isNat(V2:S)) 0.002/0.002 U33(tt) -> tt 0.002/0.002 U41(tt,N:S) -> N:S 0.002/0.002 U51(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.002/0.002 U61(tt) -> 0 0.002/0.002 U71(tt,M:S,N:S) -> plus(x(N:S,M:S),N:S) 0.002/0.002 and(tt,X:S) -> X:S 0.002/0.002 isNat(plus(V1:S,V2:S)) -> U11(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S) 0.002/0.002 isNat(x(V1:S,V2:S)) -> U31(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S) 0.002/0.002 isNat(0) -> tt 0.002/0.002 isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S) 0.002/0.002 isNatKind(plus(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S)) 0.002/0.002 isNatKind(x(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S)) 0.002/0.002 isNatKind(0) -> tt 0.002/0.002 isNatKind(s(V1:S)) -> isNatKind(V1:S) 0.002/0.002 plus(N:S,0) -> U41(and(isNat(N:S),isNatKind(N:S)),N:S) 0.002/0.002 plus(N:S,s(M:S)) -> U51(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 x(N:S,0) -> U61(and(isNat(N:S),isNatKind(N:S))) 0.002/0.002 x(N:S,s(M:S)) -> U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 CleanTRS Processor: 0.002/0.002 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S M:S N:S V1:S V2:S X:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U13 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U33 1) 0.002/0.002 (U41 1) 0.002/0.002 (U51 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (and 1) 0.002/0.002 (isNat) 0.002/0.002 (isNatKind) 0.002/0.002 (plus 1 2) 0.002/0.002 (x 1 2) 0.002/0.002 (0) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (s 1) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U11(tt,V1:S,V2:S) -> U12(isNat(V1:S),V2:S) 0.002/0.002 U12(tt,V2:S) -> U13(isNat(V2:S)) 0.002/0.002 U13(tt) -> tt 0.002/0.002 U21(tt,V1:S) -> U22(isNat(V1:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt,V1:S,V2:S) -> U32(isNat(V1:S),V2:S) 0.002/0.002 U32(tt,V2:S) -> U33(isNat(V2:S)) 0.002/0.002 U33(tt) -> tt 0.002/0.002 U41(tt,N:S) -> N:S 0.002/0.002 U51(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.002/0.002 U61(tt) -> 0 0.002/0.002 U71(tt,M:S,N:S) -> plus(x(N:S,M:S),N:S) 0.002/0.002 and(tt,X:S) -> X:S 0.002/0.002 isNat(plus(V1:S,V2:S)) -> U11(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S) 0.002/0.002 isNat(x(V1:S,V2:S)) -> U31(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S) 0.002/0.002 isNat(0) -> tt 0.002/0.002 isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S) 0.002/0.002 isNatKind(plus(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S)) 0.002/0.002 isNatKind(x(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S)) 0.002/0.002 isNatKind(0) -> tt 0.002/0.002 isNatKind(s(V1:S)) -> isNatKind(V1:S) 0.002/0.002 plus(N:S,0) -> U41(and(isNat(N:S),isNatKind(N:S)),N:S) 0.002/0.002 plus(N:S,s(M:S)) -> U51(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 x(N:S,0) -> U61(and(isNat(N:S),isNatKind(N:S))) 0.002/0.002 x(N:S,s(M:S)) -> U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 Modular Confluence Combinations Decomposition Processor: 0.002/0.002 It is a CTRS -> No modular confluence 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 CS-TRS Processor: 0.002/0.002 R is a CS-TRS 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S M:S N:S V1:S V2:S X:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U13 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U33 1) 0.002/0.002 (U41 1) 0.002/0.002 (U51 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (and 1) 0.002/0.002 (isNat) 0.002/0.002 (isNatKind) 0.002/0.002 (plus 1 2) 0.002/0.002 (x 1 2) 0.002/0.002 (0) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (s 1) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U11(tt,V1:S,V2:S) -> U12(isNat(V1:S),V2:S) 0.002/0.002 U12(tt,V2:S) -> U13(isNat(V2:S)) 0.002/0.002 U13(tt) -> tt 0.002/0.002 U21(tt,V1:S) -> U22(isNat(V1:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt,V1:S,V2:S) -> U32(isNat(V1:S),V2:S) 0.002/0.002 U32(tt,V2:S) -> U33(isNat(V2:S)) 0.002/0.002 U33(tt) -> tt 0.002/0.002 U41(tt,N:S) -> N:S 0.002/0.002 U51(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.002/0.002 U61(tt) -> 0 0.002/0.002 U71(tt,M:S,N:S) -> plus(x(N:S,M:S),N:S) 0.002/0.002 and(tt,X:S) -> X:S 0.002/0.002 isNat(plus(V1:S,V2:S)) -> U11(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S) 0.002/0.002 isNat(x(V1:S,V2:S)) -> U31(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S) 0.002/0.002 isNat(0) -> tt 0.002/0.002 isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S) 0.002/0.002 isNatKind(plus(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S)) 0.002/0.002 isNatKind(x(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S)) 0.002/0.002 isNatKind(0) -> tt 0.002/0.002 isNatKind(s(V1:S)) -> isNatKind(V1:S) 0.002/0.002 plus(N:S,0) -> U41(and(isNat(N:S),isNatKind(N:S)),N:S) 0.002/0.002 plus(N:S,s(M:S)) -> U51(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 x(N:S,0) -> U61(and(isNat(N:S),isNatKind(N:S))) 0.002/0.002 x(N:S,s(M:S)) -> U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 Extended u-Critical Pairs NonLHRV Processor [JLAMP21]: 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => plus(x29:S,0) -> U41(and(isNat(x29:S),isNatKind(x29:S)),x29:S) 0.002/0.002 Rule 22 (l' :-> r') => plus(N:S,0) -> U41(and(isNat(N:S),isNatKind(N:S)),N:S) 0.002/0.002 Var => x29:S 0.002/0.002 Pos x29:S in l => [1] 0.002/0.002 Sigma => {x29:S -> plus(N:S,0)} 0.002/0.002 s => U41(and(isNat(plus(N:S,0)),isNatKind(plus(N:S,0))),plus(N:S,0)) 0.002/0.002 t => plus(U41(and(isNat(N:S),isNatKind(N:S)),N:S),0) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => plus(x29:S,0) -> U41(and(isNat(x29:S),isNatKind(x29:S)),x29:S) 0.002/0.002 Rule 23 (l' :-> r') => plus(N:S,s(M:S)) -> U51(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 Var => x29:S 0.002/0.002 Pos x29:S in l => [1] 0.002/0.002 Sigma => {x29:S -> plus(N:S,s(M:S))} 0.002/0.002 s => U41(and(isNat(plus(N:S,s(M:S))),isNatKind(plus(N:S,s(M:S)))),plus(N:S,s(M:S))) 0.002/0.002 t => plus(U51(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S),0) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => plus(x29:S,0) -> U41(and(isNat(x29:S),isNatKind(x29:S)),x29:S) 0.002/0.002 Rule 24 (l' :-> r') => x(N:S,0) -> U61(and(isNat(N:S),isNatKind(N:S))) 0.002/0.002 Var => x29:S 0.002/0.002 Pos x29:S in l => [1] 0.002/0.002 Sigma => {x29:S -> x(N:S,0)} 0.002/0.002 s => U41(and(isNat(x(N:S,0)),isNatKind(x(N:S,0))),x(N:S,0)) 0.002/0.002 t => plus(U61(and(isNat(N:S),isNatKind(N:S))),0) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => plus(x29:S,0) -> U41(and(isNat(x29:S),isNatKind(x29:S)),x29:S) 0.002/0.002 Rule 25 (l' :-> r') => x(N:S,s(M:S)) -> U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 Var => x29:S 0.002/0.002 Pos x29:S in l => [1] 0.002/0.002 Sigma => {x29:S -> x(N:S,s(M:S))} 0.002/0.002 s => U41(and(isNat(x(N:S,s(M:S))),isNatKind(x(N:S,s(M:S)))),x(N:S,s(M:S))) 0.002/0.002 t => plus(U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S),0) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => plus(x31:S,s(x30:S)) -> U51(and(and(isNat(x30:S),isNatKind(x30:S)),and(isNat(x31:S),isNatKind(x31:S))),x30:S,x31:S) 0.002/0.002 Rule 23 (l' :-> r') => plus(N:S,s(M:S)) -> U51(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 Var => x30:S 0.002/0.002 Pos x30:S in l => [2,1] 0.002/0.002 Sigma => {x30:S -> plus(N:S,s(M:S))} 0.002/0.002 s => U51(and(and(isNat(plus(N:S,s(M:S))),isNatKind(plus(N:S,s(M:S)))),and(isNat(x31:S),isNatKind(x31:S))),plus(N:S,s(M:S)),x31:S) 0.002/0.002 t => plus(x31:S,s(U51(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S))) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => plus(x31:S,s(x30:S)) -> U51(and(and(isNat(x30:S),isNatKind(x30:S)),and(isNat(x31:S),isNatKind(x31:S))),x30:S,x31:S) 0.002/0.002 Rule 24 (l' :-> r') => x(N:S,0) -> U61(and(isNat(N:S),isNatKind(N:S))) 0.002/0.002 Var => x30:S 0.002/0.002 Pos x30:S in l => [2,1] 0.002/0.002 Sigma => {x30:S -> x(N:S,0)} 0.002/0.002 s => U51(and(and(isNat(x(N:S,0)),isNatKind(x(N:S,0))),and(isNat(x31:S),isNatKind(x31:S))),x(N:S,0),x31:S) 0.002/0.002 t => plus(x31:S,s(U61(and(isNat(N:S),isNatKind(N:S))))) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => plus(x31:S,s(x30:S)) -> U51(and(and(isNat(x30:S),isNatKind(x30:S)),and(isNat(x31:S),isNatKind(x31:S))),x30:S,x31:S) 0.002/0.002 Rule 25 (l' :-> r') => x(N:S,s(M:S)) -> U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 Var => x30:S 0.002/0.002 Pos x30:S in l => [2,1] 0.002/0.002 Sigma => {x30:S -> x(N:S,s(M:S))} 0.002/0.002 s => U51(and(and(isNat(x(N:S,s(M:S))),isNatKind(x(N:S,s(M:S)))),and(isNat(x31:S),isNatKind(x31:S))),x(N:S,s(M:S)),x31:S) 0.002/0.002 t => plus(x31:S,s(U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S))) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => x(x32:S,0) -> U61(and(isNat(x32:S),isNatKind(x32:S))) 0.002/0.002 Rule 24 (l' :-> r') => x(N:S,0) -> U61(and(isNat(N:S),isNatKind(N:S))) 0.002/0.002 Var => x32:S 0.002/0.002 Pos x32:S in l => [1] 0.002/0.002 Sigma => {x32:S -> x(N:S,0)} 0.002/0.002 s => U61(and(isNat(x(N:S,0)),isNatKind(x(N:S,0)))) 0.002/0.002 t => x(U61(and(isNat(N:S),isNatKind(N:S))),0) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => x(x32:S,0) -> U61(and(isNat(x32:S),isNatKind(x32:S))) 0.002/0.002 Rule 25 (l' :-> r') => x(N:S,s(M:S)) -> U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 Var => x32:S 0.002/0.002 Pos x32:S in l => [1] 0.002/0.002 Sigma => {x32:S -> x(N:S,s(M:S))} 0.002/0.002 s => U61(and(isNat(x(N:S,s(M:S))),isNatKind(x(N:S,s(M:S))))) 0.002/0.002 t => x(U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S),0) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 ->Extended u-Critical Pair: 0.002/0.002 Rule 1 (l :-> r) => x(x34:S,s(x33:S)) -> U71(and(and(isNat(x33:S),isNatKind(x33:S)),and(isNat(x34:S),isNatKind(x34:S))),x33:S,x34:S) 0.002/0.002 Rule 25 (l' :-> r') => x(N:S,s(M:S)) -> U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 Var => x33:S 0.002/0.002 Pos x33:S in l => [2,1] 0.002/0.002 Sigma => {x33:S -> x(N:S,s(M:S))} 0.002/0.002 s => U71(and(and(isNat(x(N:S,s(M:S))),isNatKind(x(N:S,s(M:S)))),and(isNat(x34:S),isNatKind(x34:S))),x(N:S,s(M:S)),x34:S) 0.002/0.002 t => x(x34:S,s(U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S))) 0.002/0.002 NW => 1 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S M:S N:S V1:S V2:S X:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U13 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U33 1) 0.002/0.002 (U41 1) 0.002/0.002 (U51 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (and 1) 0.002/0.002 (isNat) 0.002/0.002 (isNatKind) 0.002/0.002 (plus 1 2) 0.002/0.002 (x 1 2) 0.002/0.002 (0) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (s 1) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U11(tt,V1:S,V2:S) -> U12(isNat(V1:S),V2:S) 0.002/0.002 U12(tt,V2:S) -> U13(isNat(V2:S)) 0.002/0.002 U13(tt) -> tt 0.002/0.002 U21(tt,V1:S) -> U22(isNat(V1:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt,V1:S,V2:S) -> U32(isNat(V1:S),V2:S) 0.002/0.002 U32(tt,V2:S) -> U33(isNat(V2:S)) 0.002/0.002 U33(tt) -> tt 0.002/0.002 U41(tt,N:S) -> N:S 0.002/0.002 U51(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.002/0.002 U61(tt) -> 0 0.002/0.002 U71(tt,M:S,N:S) -> plus(x(N:S,M:S),N:S) 0.002/0.002 and(tt,X:S) -> X:S 0.002/0.002 isNat(plus(V1:S,V2:S)) -> U11(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S) 0.002/0.002 isNat(x(V1:S,V2:S)) -> U31(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S) 0.002/0.002 isNat(0) -> tt 0.002/0.002 isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S) 0.002/0.002 isNatKind(plus(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S)) 0.002/0.002 isNatKind(x(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S)) 0.002/0.002 isNatKind(0) -> tt 0.002/0.002 isNatKind(s(V1:S)) -> isNatKind(V1:S) 0.002/0.002 plus(N:S,0) -> U41(and(isNat(N:S),isNatKind(N:S)),N:S) 0.002/0.002 plus(N:S,s(M:S)) -> U51(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 x(N:S,0) -> U61(and(isNat(N:S),isNatKind(N:S))) 0.002/0.002 x(N:S,s(M:S)) -> U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 ) 0.002/0.002 Critical Pairs: 0.002/0.002 => Not trivial, Not overlay, NW1, N1 0.002/0.002 => Not trivial, Not overlay, NW1, N2 0.002/0.002 => Not trivial, Not overlay, NW1, N3 0.002/0.002 => Not trivial, Not overlay, NW1, N4 0.002/0.002 => Not trivial, Not overlay, NW1, N5 0.002/0.002 => Not trivial, Not overlay, NW1, N6 0.002/0.002 => Not trivial, Not overlay, NW1, N7 0.002/0.002 => Not trivial, Not overlay, NW1, N8 0.002/0.002 => Not trivial, Not overlay, NW1, N9 0.002/0.002 => Not trivial, Not overlay, NW1, N10 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 Huet Levy Processor: 0.002/0.002 -> Rules: 0.002/0.002 U11(tt,V1:S,V2:S) -> U12(isNat(V1:S),V2:S) 0.002/0.002 U12(tt,V2:S) -> U13(isNat(V2:S)) 0.002/0.002 U13(tt) -> tt 0.002/0.002 U21(tt,V1:S) -> U22(isNat(V1:S)) 0.002/0.002 U22(tt) -> tt 0.002/0.002 U31(tt,V1:S,V2:S) -> U32(isNat(V1:S),V2:S) 0.002/0.002 U32(tt,V2:S) -> U33(isNat(V2:S)) 0.002/0.002 U33(tt) -> tt 0.002/0.002 U41(tt,N:S) -> N:S 0.002/0.002 U51(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.002/0.002 U61(tt) -> 0 0.002/0.002 U71(tt,M:S,N:S) -> plus(x(N:S,M:S),N:S) 0.002/0.002 and(tt,X:S) -> X:S 0.002/0.002 isNat(plus(V1:S,V2:S)) -> U11(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S) 0.002/0.002 isNat(x(V1:S,V2:S)) -> U31(and(isNatKind(V1:S),isNatKind(V2:S)),V1:S,V2:S) 0.002/0.002 isNat(0) -> tt 0.002/0.002 isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S) 0.002/0.002 isNatKind(plus(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S)) 0.002/0.002 isNatKind(x(V1:S,V2:S)) -> and(isNatKind(V1:S),isNatKind(V2:S)) 0.002/0.002 isNatKind(0) -> tt 0.002/0.002 isNatKind(s(V1:S)) -> isNatKind(V1:S) 0.002/0.002 plus(N:S,0) -> U41(and(isNat(N:S),isNatKind(N:S)),N:S) 0.002/0.002 plus(N:S,s(M:S)) -> U51(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 x(N:S,0) -> U61(and(isNat(N:S),isNatKind(N:S))) 0.002/0.002 x(N:S,s(M:S)) -> U71(and(and(isNat(M:S),isNatKind(M:S)),and(isNat(N:S),isNatKind(N:S))),M:S,N:S) 0.002/0.002 -> Vars: 0.002/0.002 V1, V2, V2, V1, V1, V2, V2, N, M, N, M, N, X, V1, V2, V1, V2, V1, V1, V2, V1, V2, V1, N, M, N, N, M, N 0.002/0.002 -> UVars: 0.002/0.002 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.002/0.002 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.002/0.002 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.002/0.002 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [N], UV-LFrozen: [N], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [M, N], UV-LFrozen: [M, N], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [M, N], UV-LFrozen: [M, N], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [X], UV-LFrozen: [X], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.002/0.002 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.002/0.002 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.002/0.002 (UV-RuleId: 22, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N]) 0.002/0.002 (UV-RuleId: 23, UV-LActive: [M, N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [M, N]) 0.002/0.002 (UV-RuleId: 24, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N]) 0.002/0.002 (UV-RuleId: 25, UV-LActive: [M, N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [M, N]) 0.002/0.002 -> FVars: 0.002/0.002 x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34 0.002/0.002 -> PVars: 0.002/0.002 V1: [x6, x9, x10, x19, x21, x23, x24, x26, x28], V2: [x7, x8, x11, x12, x20, x22, x25, x27], N: [x13, x15, x17, x29, x31, x32, x34], M: [x14, x16, x30, x33], X: [x18] 0.002/0.002 0.002/0.002 -> Rlps: 0.002/0.002 (rule: U11(tt,x6:S,x7:S) -> U12(isNat(x6:S),x7:S), id: 1, possubterms: U11(tt,x6:S,x7:S)->[], tt->[1]) 0.002/0.002 (rule: U12(tt,x8:S) -> U13(isNat(x8:S)), id: 2, possubterms: U12(tt,x8:S)->[], tt->[1]) 0.002/0.002 (rule: U13(tt) -> tt, id: 3, possubterms: U13(tt)->[], tt->[1]) 0.002/0.002 (rule: U21(tt,x9:S) -> U22(isNat(x9:S)), id: 4, possubterms: U21(tt,x9:S)->[], tt->[1]) 0.002/0.002 (rule: U22(tt) -> tt, id: 5, possubterms: U22(tt)->[], tt->[1]) 0.002/0.002 (rule: U31(tt,x10:S,x11:S) -> U32(isNat(x10:S),x11:S), id: 6, possubterms: U31(tt,x10:S,x11:S)->[], tt->[1]) 0.002/0.002 (rule: U32(tt,x12:S) -> U33(isNat(x12:S)), id: 7, possubterms: U32(tt,x12:S)->[], tt->[1]) 0.002/0.002 (rule: U33(tt) -> tt, id: 8, possubterms: U33(tt)->[], tt->[1]) 0.002/0.002 (rule: U41(tt,x13:S) -> x13:S, id: 9, possubterms: U41(tt,x13:S)->[], tt->[1]) 0.002/0.002 (rule: U51(tt,x14:S,x15:S) -> s(plus(x15:S,x14:S)), id: 10, possubterms: U51(tt,x14:S,x15:S)->[], tt->[1]) 0.002/0.002 (rule: U61(tt) -> 0, id: 11, possubterms: U61(tt)->[], tt->[1]) 0.002/0.002 (rule: U71(tt,x16:S,x17:S) -> plus(x(x17:S,x16:S),x17:S), id: 12, possubterms: U71(tt,x16:S,x17:S)->[], tt->[1]) 0.002/0.002 (rule: and(tt,x18:S) -> x18:S, id: 13, possubterms: and(tt,x18:S)->[], tt->[1]) 0.002/0.002 (rule: isNat(plus(x19:S,x20:S)) -> U11(and(isNatKind(x19:S),isNatKind(x20:S)),x19:S,x20:S), id: 14, possubterms: isNat(plus(x19:S,x20:S))->[]) 0.002/0.002 (rule: isNat(x(x21:S,x22:S)) -> U31(and(isNatKind(x21:S),isNatKind(x22:S)),x21:S,x22:S), id: 15, possubterms: isNat(x(x21:S,x22:S))->[]) 0.002/0.002 (rule: isNat(0) -> tt, id: 16, possubterms: isNat(0)->[]) 0.002/0.002 (rule: isNat(s(x23:S)) -> U21(isNatKind(x23:S),x23:S), id: 17, possubterms: isNat(s(x23:S))->[]) 0.002/0.002 (rule: isNatKind(plus(x24:S,x25:S)) -> and(isNatKind(x24:S),isNatKind(x25:S)), id: 18, possubterms: isNatKind(plus(x24:S,x25:S))->[]) 0.002/0.002 (rule: isNatKind(x(x26:S,x27:S)) -> and(isNatKind(x26:S),isNatKind(x27:S)), id: 19, possubterms: isNatKind(x(x26:S,x27:S))->[]) 0.002/0.002 (rule: isNatKind(0) -> tt, id: 20, possubterms: isNatKind(0)->[]) 0.002/0.002 (rule: isNatKind(s(x28:S)) -> isNatKind(x28:S), id: 21, possubterms: isNatKind(s(x28:S))->[]) 0.002/0.002 (rule: plus(x29:S,0) -> U41(and(isNat(x29:S),isNatKind(x29:S)),x29:S), id: 22, possubterms: plus(x29:S,0)->[], 0->[2]) 0.002/0.002 (rule: plus(x31:S,s(x30:S)) -> U51(and(and(isNat(x30:S),isNatKind(x30:S)),and(isNat(x31:S),isNatKind(x31:S))),x30:S,x31:S), id: 23, possubterms: plus(x31:S,s(x30:S))->[], s(x30:S)->[2]) 0.002/0.002 (rule: x(x32:S,0) -> U61(and(isNat(x32:S),isNatKind(x32:S))), id: 24, possubterms: x(x32:S,0)->[], 0->[2]) 0.002/0.002 (rule: x(x34:S,s(x33:S)) -> U71(and(and(isNat(x33:S),isNatKind(x33:S)),and(isNat(x34:S),isNatKind(x34:S))),x33:S,x34:S), id: 25, possubterms: x(x34:S,s(x33:S))->[], s(x33:S)->[2]) 0.002/0.002 0.002/0.002 -> Unifications: 0.002/0.002 0.002/0.002 0.002/0.002 -> Critical pairs info: 0.002/0.002 => Not trivial, Not overlay, NW1, N1 0.002/0.002 => Not trivial, Not overlay, NW1, N2 0.002/0.002 => Not trivial, Not overlay, NW1, N3 0.002/0.002 => Not trivial, Not overlay, NW1, N4 0.002/0.002 => Not trivial, Not overlay, NW1, N5 0.002/0.002 => Not trivial, Not overlay, NW1, N6 0.002/0.002 => Not trivial, Not overlay, NW1, N7 0.002/0.002 => Not trivial, Not overlay, NW1, N8 0.002/0.002 => Not trivial, Not overlay, NW1, N9 0.002/0.002 => Not trivial, Not overlay, NW1, N10 0.002/0.002 0.002/0.002 -> Problem conclusions: 0.002/0.002 Left linear, Not right linear, Not linear 0.002/0.002 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.002/0.002 Not Huet-Levy confluent, Not Newman confluent 0.002/0.002 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 No Convergence Brute Force Processor: 0.002/0.002 -> Rewritings: 0.002/0.002 s: U41(and(isNat(x(N:S,0)),isNatKind(x(N:S,0))),x(N:S,0)) 0.002/0.002 Nodes: [0,1] 0.002/0.002 Edges: [(0,1)] 0.002/0.002 ID: 0 => ('U41(and(isNat(x(N:S,0)),isNatKind(x(N:S,0))),x(N:S,0))', D0) 0.002/0.002 ID: 1 => ('U41(and(U31(and(isNatKind(N:S),isNatKind(0)),N:S,0),isNatKind(x(N:S,0))),x(N:S,0))', D1, R15, P[1, 1], S{x21:S -> N:S, x22:S -> 0}), NR: 'U31(and(isNatKind(N:S),isNatKind(0)),N:S,0)' 0.002/0.002 t: plus(U61(and(isNat(N:S),isNatKind(N:S))),0) 0.002/0.002 Nodes: [0,1] 0.002/0.002 Edges: [(0,1)] 0.002/0.002 ID: 0 => ('plus(U61(and(isNat(N:S),isNatKind(N:S))),0)', D0) 0.002/0.002 ID: 1 => ('U41(and(isNat(U61(and(isNat(N:S),isNatKind(N:S)))),isNatKind(U61(and(isNat(N:S),isNatKind(N:S))))),U61(and(isNat(N:S),isNatKind(N:S))))', D1, R22, P[], S{x29:S -> U61(and(isNat(N:S),isNatKind(N:S)))}), NR: 'U41(and(isNat(U61(and(isNat(N:S),isNatKind(N:S)))),isNatKind(U61(and(isNat(N:S),isNatKind(N:S))))),U61(and(isNat(N:S),isNatKind(N:S))))' 0.002/0.002 U41(and(isNat(x(N:S,0)),isNatKind(x(N:S,0))),x(N:S,0)) ->* no union *<- plus(U61(and(isNat(N:S),isNatKind(N:S))),0) 0.002/0.002 "Not joinable" 0.002/0.002 0.002/0.002 The problem is not joinable. 0.002/0.002 0.02user 0.00system 0:00.02elapsed 91%CPU (0avgtext+0avgdata 12636maxresident)k 0.002/0.002 0inputs+0outputs (0major+1348minor)pagefaults 0swaps