0.003/0.003 NO 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 0.003/0.003 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (VAR vNonEmpty:S M:S N:S V1:S V2:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (U101 1) 0.003/0.003 (U102 1) 0.003/0.003 (U103 1) 0.003/0.003 (U104 1) 0.003/0.003 (U11 1) 0.003/0.003 (U12 1) 0.003/0.003 (U13 1) 0.003/0.003 (U14 1) 0.003/0.003 (U15 1) 0.003/0.003 (U16 1) 0.003/0.003 (U21 1) 0.003/0.003 (U22 1) 0.003/0.003 (U23 1) 0.003/0.003 (U31 1) 0.003/0.003 (U32 1) 0.003/0.003 (U33 1) 0.003/0.003 (U34 1) 0.003/0.003 (U35 1) 0.003/0.003 (U36 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U51 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U72 1) 0.003/0.003 (U81 1) 0.003/0.003 (U82 1) 0.003/0.003 (U83 1) 0.003/0.003 (U84 1) 0.003/0.003 (U91 1) 0.003/0.003 (U92 1) 0.003/0.003 (isNat) 0.003/0.003 (isNatKind) 0.003/0.003 (plus 1 2) 0.003/0.003 (x 1 2) 0.003/0.003 (0) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (s 1) 0.003/0.003 (tt) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 U101(tt,M:S,N:S) -> U102(isNatKind(M:S),M:S,N:S) 0.003/0.003 U102(tt,M:S,N:S) -> U103(isNat(N:S),M:S,N:S) 0.003/0.003 U103(tt,M:S,N:S) -> U104(isNatKind(N:S),M:S,N:S) 0.003/0.003 U104(tt,M:S,N:S) -> plus(x(N:S,M:S),N:S) 0.003/0.003 U11(tt,V1:S,V2:S) -> U12(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 U12(tt,V1:S,V2:S) -> U13(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U13(tt,V1:S,V2:S) -> U14(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U14(tt,V1:S,V2:S) -> U15(isNat(V1:S),V2:S) 0.003/0.003 U15(tt,V2:S) -> U16(isNat(V2:S)) 0.003/0.003 U16(tt) -> tt 0.003/0.003 U21(tt,V1:S) -> U22(isNatKind(V1:S),V1:S) 0.003/0.003 U22(tt,V1:S) -> U23(isNat(V1:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V1:S,V2:S) -> U32(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 U32(tt,V1:S,V2:S) -> U33(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U33(tt,V1:S,V2:S) -> U34(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U34(tt,V1:S,V2:S) -> U35(isNat(V1:S),V2:S) 0.003/0.003 U35(tt,V2:S) -> U36(isNat(V2:S)) 0.003/0.003 U36(tt) -> tt 0.003/0.003 U41(tt,V2:S) -> U42(isNatKind(V2:S)) 0.003/0.003 U42(tt) -> tt 0.003/0.003 U51(tt) -> tt 0.003/0.003 U61(tt,V2:S) -> U62(isNatKind(V2:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,N:S) -> U72(isNatKind(N:S),N:S) 0.003/0.003 U72(tt,N:S) -> N:S 0.003/0.003 U81(tt,M:S,N:S) -> U82(isNatKind(M:S),M:S,N:S) 0.003/0.003 U82(tt,M:S,N:S) -> U83(isNat(N:S),M:S,N:S) 0.003/0.003 U83(tt,M:S,N:S) -> U84(isNatKind(N:S),M:S,N:S) 0.003/0.003 U84(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.003/0.003 U91(tt,N:S) -> U92(isNatKind(N:S)) 0.003/0.003 U92(tt) -> 0 0.003/0.003 isNat(plus(V1:S,V2:S)) -> U11(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 isNat(x(V1:S,V2:S)) -> U31(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 isNat(0) -> tt 0.003/0.003 isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S) 0.003/0.003 isNatKind(plus(V1:S,V2:S)) -> U41(isNatKind(V1:S),V2:S) 0.003/0.003 isNatKind(x(V1:S,V2:S)) -> U61(isNatKind(V1:S),V2:S) 0.003/0.003 isNatKind(0) -> tt 0.003/0.003 isNatKind(s(V1:S)) -> U51(isNatKind(V1:S)) 0.003/0.003 plus(N:S,0) -> U71(isNat(N:S),N:S) 0.003/0.003 plus(N:S,s(M:S)) -> U81(isNat(M:S),M:S,N:S) 0.003/0.003 x(N:S,0) -> U91(isNat(N:S),N:S) 0.003/0.003 x(N:S,s(M:S)) -> U101(isNat(M:S),M:S,N:S) 0.003/0.003 ) 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 0.003/0.003 CleanTRS Processor: 0.003/0.003 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (VAR vNonEmpty:S M:S N:S V1:S V2:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (U101 1) 0.003/0.003 (U102 1) 0.003/0.003 (U103 1) 0.003/0.003 (U104 1) 0.003/0.003 (U11 1) 0.003/0.003 (U12 1) 0.003/0.003 (U13 1) 0.003/0.003 (U14 1) 0.003/0.003 (U15 1) 0.003/0.003 (U16 1) 0.003/0.003 (U21 1) 0.003/0.003 (U22 1) 0.003/0.003 (U23 1) 0.003/0.003 (U31 1) 0.003/0.003 (U32 1) 0.003/0.003 (U33 1) 0.003/0.003 (U34 1) 0.003/0.003 (U35 1) 0.003/0.003 (U36 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U51 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U72 1) 0.003/0.003 (U81 1) 0.003/0.003 (U82 1) 0.003/0.003 (U83 1) 0.003/0.003 (U84 1) 0.003/0.003 (U91 1) 0.003/0.003 (U92 1) 0.003/0.003 (isNat) 0.003/0.003 (isNatKind) 0.003/0.003 (plus 1 2) 0.003/0.003 (x 1 2) 0.003/0.003 (0) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (s 1) 0.003/0.003 (tt) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 U101(tt,M:S,N:S) -> U102(isNatKind(M:S),M:S,N:S) 0.003/0.003 U102(tt,M:S,N:S) -> U103(isNat(N:S),M:S,N:S) 0.003/0.003 U103(tt,M:S,N:S) -> U104(isNatKind(N:S),M:S,N:S) 0.003/0.003 U104(tt,M:S,N:S) -> plus(x(N:S,M:S),N:S) 0.003/0.003 U11(tt,V1:S,V2:S) -> U12(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 U12(tt,V1:S,V2:S) -> U13(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U13(tt,V1:S,V2:S) -> U14(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U14(tt,V1:S,V2:S) -> U15(isNat(V1:S),V2:S) 0.003/0.003 U15(tt,V2:S) -> U16(isNat(V2:S)) 0.003/0.003 U16(tt) -> tt 0.003/0.003 U21(tt,V1:S) -> U22(isNatKind(V1:S),V1:S) 0.003/0.003 U22(tt,V1:S) -> U23(isNat(V1:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V1:S,V2:S) -> U32(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 U32(tt,V1:S,V2:S) -> U33(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U33(tt,V1:S,V2:S) -> U34(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U34(tt,V1:S,V2:S) -> U35(isNat(V1:S),V2:S) 0.003/0.003 U35(tt,V2:S) -> U36(isNat(V2:S)) 0.003/0.003 U36(tt) -> tt 0.003/0.003 U41(tt,V2:S) -> U42(isNatKind(V2:S)) 0.003/0.003 U42(tt) -> tt 0.003/0.003 U51(tt) -> tt 0.003/0.003 U61(tt,V2:S) -> U62(isNatKind(V2:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,N:S) -> U72(isNatKind(N:S),N:S) 0.003/0.003 U72(tt,N:S) -> N:S 0.003/0.003 U81(tt,M:S,N:S) -> U82(isNatKind(M:S),M:S,N:S) 0.003/0.003 U82(tt,M:S,N:S) -> U83(isNat(N:S),M:S,N:S) 0.003/0.003 U83(tt,M:S,N:S) -> U84(isNatKind(N:S),M:S,N:S) 0.003/0.003 U84(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.003/0.003 U91(tt,N:S) -> U92(isNatKind(N:S)) 0.003/0.003 U92(tt) -> 0 0.003/0.003 isNat(plus(V1:S,V2:S)) -> U11(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 isNat(x(V1:S,V2:S)) -> U31(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 isNat(0) -> tt 0.003/0.003 isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S) 0.003/0.003 isNatKind(plus(V1:S,V2:S)) -> U41(isNatKind(V1:S),V2:S) 0.003/0.003 isNatKind(x(V1:S,V2:S)) -> U61(isNatKind(V1:S),V2:S) 0.003/0.003 isNatKind(0) -> tt 0.003/0.003 isNatKind(s(V1:S)) -> U51(isNatKind(V1:S)) 0.003/0.003 plus(N:S,0) -> U71(isNat(N:S),N:S) 0.003/0.003 plus(N:S,s(M:S)) -> U81(isNat(M:S),M:S,N:S) 0.003/0.003 x(N:S,0) -> U91(isNat(N:S),N:S) 0.003/0.003 x(N:S,s(M:S)) -> U101(isNat(M:S),M:S,N:S) 0.003/0.003 ) 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 0.003/0.003 Modular Confluence Combinations Decomposition Processor: 0.003/0.003 It is a CTRS -> No modular confluence 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 CS-TRS Processor: 0.003/0.003 R is a CS-TRS 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (VAR vNonEmpty:S M:S N:S V1:S V2:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (U101 1) 0.003/0.003 (U102 1) 0.003/0.003 (U103 1) 0.003/0.003 (U104 1) 0.003/0.003 (U11 1) 0.003/0.003 (U12 1) 0.003/0.003 (U13 1) 0.003/0.003 (U14 1) 0.003/0.003 (U15 1) 0.003/0.003 (U16 1) 0.003/0.003 (U21 1) 0.003/0.003 (U22 1) 0.003/0.003 (U23 1) 0.003/0.003 (U31 1) 0.003/0.003 (U32 1) 0.003/0.003 (U33 1) 0.003/0.003 (U34 1) 0.003/0.003 (U35 1) 0.003/0.003 (U36 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U51 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U72 1) 0.003/0.003 (U81 1) 0.003/0.003 (U82 1) 0.003/0.003 (U83 1) 0.003/0.003 (U84 1) 0.003/0.003 (U91 1) 0.003/0.003 (U92 1) 0.003/0.003 (isNat) 0.003/0.003 (isNatKind) 0.003/0.003 (plus 1 2) 0.003/0.003 (x 1 2) 0.003/0.003 (0) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (s 1) 0.003/0.003 (tt) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 U101(tt,M:S,N:S) -> U102(isNatKind(M:S),M:S,N:S) 0.003/0.003 U102(tt,M:S,N:S) -> U103(isNat(N:S),M:S,N:S) 0.003/0.003 U103(tt,M:S,N:S) -> U104(isNatKind(N:S),M:S,N:S) 0.003/0.003 U104(tt,M:S,N:S) -> plus(x(N:S,M:S),N:S) 0.003/0.003 U11(tt,V1:S,V2:S) -> U12(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 U12(tt,V1:S,V2:S) -> U13(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U13(tt,V1:S,V2:S) -> U14(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U14(tt,V1:S,V2:S) -> U15(isNat(V1:S),V2:S) 0.003/0.003 U15(tt,V2:S) -> U16(isNat(V2:S)) 0.003/0.003 U16(tt) -> tt 0.003/0.003 U21(tt,V1:S) -> U22(isNatKind(V1:S),V1:S) 0.003/0.003 U22(tt,V1:S) -> U23(isNat(V1:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V1:S,V2:S) -> U32(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 U32(tt,V1:S,V2:S) -> U33(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U33(tt,V1:S,V2:S) -> U34(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U34(tt,V1:S,V2:S) -> U35(isNat(V1:S),V2:S) 0.003/0.003 U35(tt,V2:S) -> U36(isNat(V2:S)) 0.003/0.003 U36(tt) -> tt 0.003/0.003 U41(tt,V2:S) -> U42(isNatKind(V2:S)) 0.003/0.003 U42(tt) -> tt 0.003/0.003 U51(tt) -> tt 0.003/0.003 U61(tt,V2:S) -> U62(isNatKind(V2:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,N:S) -> U72(isNatKind(N:S),N:S) 0.003/0.003 U72(tt,N:S) -> N:S 0.003/0.003 U81(tt,M:S,N:S) -> U82(isNatKind(M:S),M:S,N:S) 0.003/0.003 U82(tt,M:S,N:S) -> U83(isNat(N:S),M:S,N:S) 0.003/0.003 U83(tt,M:S,N:S) -> U84(isNatKind(N:S),M:S,N:S) 0.003/0.003 U84(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.003/0.003 U91(tt,N:S) -> U92(isNatKind(N:S)) 0.003/0.003 U92(tt) -> 0 0.003/0.003 isNat(plus(V1:S,V2:S)) -> U11(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 isNat(x(V1:S,V2:S)) -> U31(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 isNat(0) -> tt 0.003/0.003 isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S) 0.003/0.003 isNatKind(plus(V1:S,V2:S)) -> U41(isNatKind(V1:S),V2:S) 0.003/0.003 isNatKind(x(V1:S,V2:S)) -> U61(isNatKind(V1:S),V2:S) 0.003/0.003 isNatKind(0) -> tt 0.003/0.003 isNatKind(s(V1:S)) -> U51(isNatKind(V1:S)) 0.003/0.003 plus(N:S,0) -> U71(isNat(N:S),N:S) 0.003/0.003 plus(N:S,s(M:S)) -> U81(isNat(M:S),M:S,N:S) 0.003/0.003 x(N:S,0) -> U91(isNat(N:S),N:S) 0.003/0.003 x(N:S,s(M:S)) -> U101(isNat(M:S),M:S,N:S) 0.003/0.003 ) 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 Extended u-Critical Pairs NonLHRV Processor [JLAMP21]: 0.003/0.003 ->Extended u-Critical Pair: 0.003/0.003 Rule 1 (l :-> r) => plus(x56:S,0) -> U71(isNat(x56:S),x56:S) 0.003/0.003 Rule 41 (l' :-> r') => plus(N:S,0) -> U71(isNat(N:S),N:S) 0.003/0.003 Var => x56:S 0.003/0.003 Pos x56:S in l => [1] 0.003/0.003 Sigma => {x56:S -> plus(N:S,0)} 0.003/0.003 s => U71(isNat(plus(N:S,0)),plus(N:S,0)) 0.003/0.003 t => plus(U71(isNat(N:S),N:S),0) 0.003/0.003 NW => 1 0.003/0.003 0.003/0.003 0.003/0.003 ->Extended u-Critical Pair: 0.003/0.003 Rule 1 (l :-> r) => plus(x56:S,0) -> U71(isNat(x56:S),x56:S) 0.003/0.003 Rule 42 (l' :-> r') => plus(N:S,s(M:S)) -> U81(isNat(M:S),M:S,N:S) 0.003/0.003 Var => x56:S 0.003/0.003 Pos x56:S in l => [1] 0.003/0.003 Sigma => {x56:S -> plus(N:S,s(M:S))} 0.003/0.003 s => U71(isNat(plus(N:S,s(M:S))),plus(N:S,s(M:S))) 0.003/0.003 t => plus(U81(isNat(M:S),M:S,N:S),0) 0.003/0.003 NW => 1 0.003/0.003 0.003/0.003 0.003/0.003 ->Extended u-Critical Pair: 0.003/0.003 Rule 1 (l :-> r) => plus(x56:S,0) -> U71(isNat(x56:S),x56:S) 0.003/0.003 Rule 43 (l' :-> r') => x(N:S,0) -> U91(isNat(N:S),N:S) 0.003/0.003 Var => x56:S 0.003/0.003 Pos x56:S in l => [1] 0.003/0.003 Sigma => {x56:S -> x(N:S,0)} 0.003/0.003 s => U71(isNat(x(N:S,0)),x(N:S,0)) 0.003/0.003 t => plus(U91(isNat(N:S),N:S),0) 0.003/0.003 NW => 1 0.003/0.003 0.003/0.003 0.003/0.003 ->Extended u-Critical Pair: 0.003/0.003 Rule 1 (l :-> r) => plus(x56:S,0) -> U71(isNat(x56:S),x56:S) 0.003/0.003 Rule 44 (l' :-> r') => x(N:S,s(M:S)) -> U101(isNat(M:S),M:S,N:S) 0.003/0.003 Var => x56:S 0.003/0.003 Pos x56:S in l => [1] 0.003/0.003 Sigma => {x56:S -> x(N:S,s(M:S))} 0.003/0.003 s => U71(isNat(x(N:S,s(M:S))),x(N:S,s(M:S))) 0.003/0.003 t => plus(U101(isNat(M:S),M:S,N:S),0) 0.003/0.003 NW => 1 0.003/0.003 0.003/0.003 0.003/0.003 ->Extended u-Critical Pair: 0.003/0.003 Rule 1 (l :-> r) => plus(x58:S,s(x57:S)) -> U81(isNat(x57:S),x57:S,x58:S) 0.003/0.003 Rule 42 (l' :-> r') => plus(N:S,s(M:S)) -> U81(isNat(M:S),M:S,N:S) 0.003/0.003 Var => x57:S 0.003/0.003 Pos x57:S in l => [2,1] 0.003/0.003 Sigma => {x57:S -> plus(N:S,s(M:S))} 0.003/0.003 s => U81(isNat(plus(N:S,s(M:S))),plus(N:S,s(M:S)),x58:S) 0.003/0.003 t => plus(x58:S,s(U81(isNat(M:S),M:S,N:S))) 0.003/0.003 NW => 1 0.003/0.003 0.003/0.003 0.003/0.003 ->Extended u-Critical Pair: 0.003/0.003 Rule 1 (l :-> r) => plus(x58:S,s(x57:S)) -> U81(isNat(x57:S),x57:S,x58:S) 0.003/0.003 Rule 43 (l' :-> r') => x(N:S,0) -> U91(isNat(N:S),N:S) 0.003/0.003 Var => x57:S 0.003/0.003 Pos x57:S in l => [2,1] 0.003/0.003 Sigma => {x57:S -> x(N:S,0)} 0.003/0.003 s => U81(isNat(x(N:S,0)),x(N:S,0),x58:S) 0.003/0.003 t => plus(x58:S,s(U91(isNat(N:S),N:S))) 0.003/0.003 NW => 1 0.003/0.003 0.003/0.003 0.003/0.003 ->Extended u-Critical Pair: 0.003/0.003 Rule 1 (l :-> r) => plus(x58:S,s(x57:S)) -> U81(isNat(x57:S),x57:S,x58:S) 0.003/0.003 Rule 44 (l' :-> r') => x(N:S,s(M:S)) -> U101(isNat(M:S),M:S,N:S) 0.003/0.003 Var => x57:S 0.003/0.003 Pos x57:S in l => [2,1] 0.003/0.003 Sigma => {x57:S -> x(N:S,s(M:S))} 0.003/0.003 s => U81(isNat(x(N:S,s(M:S))),x(N:S,s(M:S)),x58:S) 0.003/0.003 t => plus(x58:S,s(U101(isNat(M:S),M:S,N:S))) 0.003/0.003 NW => 1 0.003/0.003 0.003/0.003 0.003/0.003 ->Extended u-Critical Pair: 0.003/0.003 Rule 1 (l :-> r) => x(x59:S,0) -> U91(isNat(x59:S),x59:S) 0.003/0.003 Rule 43 (l' :-> r') => x(N:S,0) -> U91(isNat(N:S),N:S) 0.003/0.003 Var => x59:S 0.003/0.003 Pos x59:S in l => [1] 0.003/0.003 Sigma => {x59:S -> x(N:S,0)} 0.003/0.003 s => U91(isNat(x(N:S,0)),x(N:S,0)) 0.003/0.003 t => x(U91(isNat(N:S),N:S),0) 0.003/0.003 NW => 1 0.003/0.003 0.003/0.003 0.003/0.003 ->Extended u-Critical Pair: 0.003/0.003 Rule 1 (l :-> r) => x(x59:S,0) -> U91(isNat(x59:S),x59:S) 0.003/0.003 Rule 44 (l' :-> r') => x(N:S,s(M:S)) -> U101(isNat(M:S),M:S,N:S) 0.003/0.003 Var => x59:S 0.003/0.003 Pos x59:S in l => [1] 0.003/0.003 Sigma => {x59:S -> x(N:S,s(M:S))} 0.003/0.003 s => U91(isNat(x(N:S,s(M:S))),x(N:S,s(M:S))) 0.003/0.003 t => x(U101(isNat(M:S),M:S,N:S),0) 0.003/0.003 NW => 1 0.003/0.003 0.003/0.003 0.003/0.003 ->Extended u-Critical Pair: 0.003/0.003 Rule 1 (l :-> r) => x(x61:S,s(x60:S)) -> U101(isNat(x60:S),x60:S,x61:S) 0.003/0.003 Rule 44 (l' :-> r') => x(N:S,s(M:S)) -> U101(isNat(M:S),M:S,N:S) 0.003/0.003 Var => x60:S 0.003/0.003 Pos x60:S in l => [2,1] 0.003/0.003 Sigma => {x60:S -> x(N:S,s(M:S))} 0.003/0.003 s => U101(isNat(x(N:S,s(M:S))),x(N:S,s(M:S)),x61:S) 0.003/0.003 t => x(x61:S,s(U101(isNat(M:S),M:S,N:S))) 0.003/0.003 NW => 1 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (VAR vNonEmpty:S M:S N:S V1:S V2:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (U101 1) 0.003/0.003 (U102 1) 0.003/0.003 (U103 1) 0.003/0.003 (U104 1) 0.003/0.003 (U11 1) 0.003/0.003 (U12 1) 0.003/0.003 (U13 1) 0.003/0.003 (U14 1) 0.003/0.003 (U15 1) 0.003/0.003 (U16 1) 0.003/0.003 (U21 1) 0.003/0.003 (U22 1) 0.003/0.003 (U23 1) 0.003/0.003 (U31 1) 0.003/0.003 (U32 1) 0.003/0.003 (U33 1) 0.003/0.003 (U34 1) 0.003/0.003 (U35 1) 0.003/0.003 (U36 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U51 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U72 1) 0.003/0.003 (U81 1) 0.003/0.003 (U82 1) 0.003/0.003 (U83 1) 0.003/0.003 (U84 1) 0.003/0.003 (U91 1) 0.003/0.003 (U92 1) 0.003/0.003 (isNat) 0.003/0.003 (isNatKind) 0.003/0.003 (plus 1 2) 0.003/0.003 (x 1 2) 0.003/0.003 (0) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (s 1) 0.003/0.003 (tt) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 U101(tt,M:S,N:S) -> U102(isNatKind(M:S),M:S,N:S) 0.003/0.003 U102(tt,M:S,N:S) -> U103(isNat(N:S),M:S,N:S) 0.003/0.003 U103(tt,M:S,N:S) -> U104(isNatKind(N:S),M:S,N:S) 0.003/0.003 U104(tt,M:S,N:S) -> plus(x(N:S,M:S),N:S) 0.003/0.003 U11(tt,V1:S,V2:S) -> U12(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 U12(tt,V1:S,V2:S) -> U13(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U13(tt,V1:S,V2:S) -> U14(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U14(tt,V1:S,V2:S) -> U15(isNat(V1:S),V2:S) 0.003/0.003 U15(tt,V2:S) -> U16(isNat(V2:S)) 0.003/0.003 U16(tt) -> tt 0.003/0.003 U21(tt,V1:S) -> U22(isNatKind(V1:S),V1:S) 0.003/0.003 U22(tt,V1:S) -> U23(isNat(V1:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V1:S,V2:S) -> U32(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 U32(tt,V1:S,V2:S) -> U33(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U33(tt,V1:S,V2:S) -> U34(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U34(tt,V1:S,V2:S) -> U35(isNat(V1:S),V2:S) 0.003/0.003 U35(tt,V2:S) -> U36(isNat(V2:S)) 0.003/0.003 U36(tt) -> tt 0.003/0.003 U41(tt,V2:S) -> U42(isNatKind(V2:S)) 0.003/0.003 U42(tt) -> tt 0.003/0.003 U51(tt) -> tt 0.003/0.003 U61(tt,V2:S) -> U62(isNatKind(V2:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,N:S) -> U72(isNatKind(N:S),N:S) 0.003/0.003 U72(tt,N:S) -> N:S 0.003/0.003 U81(tt,M:S,N:S) -> U82(isNatKind(M:S),M:S,N:S) 0.003/0.003 U82(tt,M:S,N:S) -> U83(isNat(N:S),M:S,N:S) 0.003/0.003 U83(tt,M:S,N:S) -> U84(isNatKind(N:S),M:S,N:S) 0.003/0.003 U84(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.003/0.003 U91(tt,N:S) -> U92(isNatKind(N:S)) 0.003/0.003 U92(tt) -> 0 0.003/0.003 isNat(plus(V1:S,V2:S)) -> U11(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 isNat(x(V1:S,V2:S)) -> U31(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 isNat(0) -> tt 0.003/0.003 isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S) 0.003/0.003 isNatKind(plus(V1:S,V2:S)) -> U41(isNatKind(V1:S),V2:S) 0.003/0.003 isNatKind(x(V1:S,V2:S)) -> U61(isNatKind(V1:S),V2:S) 0.003/0.003 isNatKind(0) -> tt 0.003/0.003 isNatKind(s(V1:S)) -> U51(isNatKind(V1:S)) 0.003/0.003 plus(N:S,0) -> U71(isNat(N:S),N:S) 0.003/0.003 plus(N:S,s(M:S)) -> U81(isNat(M:S),M:S,N:S) 0.003/0.003 x(N:S,0) -> U91(isNat(N:S),N:S) 0.003/0.003 x(N:S,s(M:S)) -> U101(isNat(M:S),M:S,N:S) 0.003/0.003 ) 0.003/0.003 Critical Pairs: 0.003/0.003 => Not trivial, Not overlay, NW1, N1 0.003/0.003 => Not trivial, Not overlay, NW1, N2 0.003/0.003 => Not trivial, Not overlay, NW1, N3 0.003/0.003 => Not trivial, Not overlay, NW1, N4 0.003/0.003 => Not trivial, Not overlay, NW1, N5 0.003/0.003 => Not trivial, Not overlay, NW1, N6 0.003/0.003 => Not trivial, Not overlay, NW1, N7 0.003/0.003 => Not trivial, Not overlay, NW1, N8 0.003/0.003 => Not trivial, Not overlay, NW1, N9 0.003/0.003 => Not trivial, Not overlay, NW1, N10 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 Huet Levy Processor: 0.003/0.003 -> Rules: 0.003/0.003 U101(tt,M:S,N:S) -> U102(isNatKind(M:S),M:S,N:S) 0.003/0.003 U102(tt,M:S,N:S) -> U103(isNat(N:S),M:S,N:S) 0.003/0.003 U103(tt,M:S,N:S) -> U104(isNatKind(N:S),M:S,N:S) 0.003/0.003 U104(tt,M:S,N:S) -> plus(x(N:S,M:S),N:S) 0.003/0.003 U11(tt,V1:S,V2:S) -> U12(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 U12(tt,V1:S,V2:S) -> U13(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U13(tt,V1:S,V2:S) -> U14(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U14(tt,V1:S,V2:S) -> U15(isNat(V1:S),V2:S) 0.003/0.003 U15(tt,V2:S) -> U16(isNat(V2:S)) 0.003/0.003 U16(tt) -> tt 0.003/0.003 U21(tt,V1:S) -> U22(isNatKind(V1:S),V1:S) 0.003/0.003 U22(tt,V1:S) -> U23(isNat(V1:S)) 0.003/0.003 U23(tt) -> tt 0.003/0.003 U31(tt,V1:S,V2:S) -> U32(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 U32(tt,V1:S,V2:S) -> U33(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U33(tt,V1:S,V2:S) -> U34(isNatKind(V2:S),V1:S,V2:S) 0.003/0.003 U34(tt,V1:S,V2:S) -> U35(isNat(V1:S),V2:S) 0.003/0.003 U35(tt,V2:S) -> U36(isNat(V2:S)) 0.003/0.003 U36(tt) -> tt 0.003/0.003 U41(tt,V2:S) -> U42(isNatKind(V2:S)) 0.003/0.003 U42(tt) -> tt 0.003/0.003 U51(tt) -> tt 0.003/0.003 U61(tt,V2:S) -> U62(isNatKind(V2:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,N:S) -> U72(isNatKind(N:S),N:S) 0.003/0.003 U72(tt,N:S) -> N:S 0.003/0.003 U81(tt,M:S,N:S) -> U82(isNatKind(M:S),M:S,N:S) 0.003/0.003 U82(tt,M:S,N:S) -> U83(isNat(N:S),M:S,N:S) 0.003/0.003 U83(tt,M:S,N:S) -> U84(isNatKind(N:S),M:S,N:S) 0.003/0.003 U84(tt,M:S,N:S) -> s(plus(N:S,M:S)) 0.003/0.003 U91(tt,N:S) -> U92(isNatKind(N:S)) 0.003/0.003 U92(tt) -> 0 0.003/0.003 isNat(plus(V1:S,V2:S)) -> U11(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 isNat(x(V1:S,V2:S)) -> U31(isNatKind(V1:S),V1:S,V2:S) 0.003/0.003 isNat(0) -> tt 0.003/0.003 isNat(s(V1:S)) -> U21(isNatKind(V1:S),V1:S) 0.003/0.003 isNatKind(plus(V1:S,V2:S)) -> U41(isNatKind(V1:S),V2:S) 0.003/0.003 isNatKind(x(V1:S,V2:S)) -> U61(isNatKind(V1:S),V2:S) 0.003/0.003 isNatKind(0) -> tt 0.003/0.003 isNatKind(s(V1:S)) -> U51(isNatKind(V1:S)) 0.003/0.003 plus(N:S,0) -> U71(isNat(N:S),N:S) 0.003/0.003 plus(N:S,s(M:S)) -> U81(isNat(M:S),M:S,N:S) 0.003/0.003 x(N:S,0) -> U91(isNat(N:S),N:S) 0.003/0.003 x(N:S,s(M:S)) -> U101(isNat(M:S),M:S,N:S) 0.003/0.003 -> Vars: 0.003/0.003 M, N, M, N, M, N, M, N, V1, V2, V1, V2, V1, V2, V1, V2, V2, V1, V1, V1, V2, V1, V2, V1, V2, V1, V2, V2, V2, V2, N, N, M, N, M, N, M, N, M, N, N, V1, V2, V1, V2, V1, V1, V2, V1, V2, V1, N, M, N, N, M, N 0.003/0.003 -> UVars: 0.003/0.003 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [M, N], UV-RFrozen: [M, N]) 0.003/0.003 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [M, N], UV-RFrozen: [M, N]) 0.003/0.003 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [M, N], UV-RFrozen: [M, N]) 0.003/0.003 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [M, N], UV-LFrozen: [M, N], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.003/0.003 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.003/0.003 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.003/0.003 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.003/0.003 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.003/0.003 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.003/0.003 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.003/0.003 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.003/0.003 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.003/0.003 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.003/0.003 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.003/0.003 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.003/0.003 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.003/0.003 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.003/0.003 (UV-RuleId: 24, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N], UV-RFrozen: [N]) 0.003/0.003 (UV-RuleId: 26, UV-LActive: [], UV-RActive: [N], UV-LFrozen: [N], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 27, UV-LActive: [], UV-RActive: [], UV-LFrozen: [M, N], UV-RFrozen: [M, N]) 0.003/0.003 (UV-RuleId: 28, UV-LActive: [], UV-RActive: [], UV-LFrozen: [M, N], UV-RFrozen: [M, N]) 0.003/0.003 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [], UV-LFrozen: [M, N], UV-RFrozen: [M, N]) 0.003/0.003 (UV-RuleId: 30, UV-LActive: [], UV-RActive: [M, N], UV-LFrozen: [M, N], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 31, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N], UV-RFrozen: [N]) 0.003/0.003 (UV-RuleId: 32, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 33, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.003/0.003 (UV-RuleId: 34, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.003/0.003 (UV-RuleId: 35, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.003/0.003 (UV-RuleId: 37, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.003/0.003 (UV-RuleId: 38, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.003/0.003 (UV-RuleId: 39, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 40, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.003/0.003 (UV-RuleId: 41, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N]) 0.003/0.003 (UV-RuleId: 42, UV-LActive: [M, N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [M, N]) 0.003/0.003 (UV-RuleId: 43, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N]) 0.003/0.003 (UV-RuleId: 44, UV-LActive: [M, N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [M, N]) 0.003/0.003 -> FVars: 0.003/0.003 x5, 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, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61 0.003/0.003 -> PVars: 0.003/0.003 M: [x5, x7, x9, x11, x37, x39, x41, x43, x57, x60], N: [x6, x8, x10, x12, x35, x36, x38, x40, x42, x44, x45, x56, x58, x59, x61], V1: [x13, x15, x17, x19, x22, x23, x24, x26, x28, x30, x46, x48, x50, x51, x53, x55], V2: [x14, x16, x18, x20, x21, x25, x27, x29, x31, x32, x33, x34, x47, x49, x52, x54] 0.003/0.003 0.003/0.003 -> Rlps: 0.003/0.003 (rule: U101(tt,x5:S,x6:S) -> U102(isNatKind(x5:S),x5:S,x6:S), id: 1, possubterms: U101(tt,x5:S,x6:S)->[], tt->[1]) 0.003/0.003 (rule: U102(tt,x7:S,x8:S) -> U103(isNat(x8:S),x7:S,x8:S), id: 2, possubterms: U102(tt,x7:S,x8:S)->[], tt->[1]) 0.003/0.003 (rule: U103(tt,x9:S,x10:S) -> U104(isNatKind(x10:S),x9:S,x10:S), id: 3, possubterms: U103(tt,x9:S,x10:S)->[], tt->[1]) 0.003/0.003 (rule: U104(tt,x11:S,x12:S) -> plus(x(x12:S,x11:S),x12:S), id: 4, possubterms: U104(tt,x11:S,x12:S)->[], tt->[1]) 0.003/0.003 (rule: U11(tt,x13:S,x14:S) -> U12(isNatKind(x13:S),x13:S,x14:S), id: 5, possubterms: U11(tt,x13:S,x14:S)->[], tt->[1]) 0.003/0.003 (rule: U12(tt,x15:S,x16:S) -> U13(isNatKind(x16:S),x15:S,x16:S), id: 6, possubterms: U12(tt,x15:S,x16:S)->[], tt->[1]) 0.003/0.003 (rule: U13(tt,x17:S,x18:S) -> U14(isNatKind(x18:S),x17:S,x18:S), id: 7, possubterms: U13(tt,x17:S,x18:S)->[], tt->[1]) 0.003/0.003 (rule: U14(tt,x19:S,x20:S) -> U15(isNat(x19:S),x20:S), id: 8, possubterms: U14(tt,x19:S,x20:S)->[], tt->[1]) 0.003/0.003 (rule: U15(tt,x21:S) -> U16(isNat(x21:S)), id: 9, possubterms: U15(tt,x21:S)->[], tt->[1]) 0.003/0.003 (rule: U16(tt) -> tt, id: 10, possubterms: U16(tt)->[], tt->[1]) 0.003/0.003 (rule: U21(tt,x22:S) -> U22(isNatKind(x22:S),x22:S), id: 11, possubterms: U21(tt,x22:S)->[], tt->[1]) 0.003/0.003 (rule: U22(tt,x23:S) -> U23(isNat(x23:S)), id: 12, possubterms: U22(tt,x23:S)->[], tt->[1]) 0.003/0.003 (rule: U23(tt) -> tt, id: 13, possubterms: U23(tt)->[], tt->[1]) 0.003/0.003 (rule: U31(tt,x24:S,x25:S) -> U32(isNatKind(x24:S),x24:S,x25:S), id: 14, possubterms: U31(tt,x24:S,x25:S)->[], tt->[1]) 0.003/0.003 (rule: U32(tt,x26:S,x27:S) -> U33(isNatKind(x27:S),x26:S,x27:S), id: 15, possubterms: U32(tt,x26:S,x27:S)->[], tt->[1]) 0.003/0.003 (rule: U33(tt,x28:S,x29:S) -> U34(isNatKind(x29:S),x28:S,x29:S), id: 16, possubterms: U33(tt,x28:S,x29:S)->[], tt->[1]) 0.003/0.003 (rule: U34(tt,x30:S,x31:S) -> U35(isNat(x30:S),x31:S), id: 17, possubterms: U34(tt,x30:S,x31:S)->[], tt->[1]) 0.003/0.003 (rule: U35(tt,x32:S) -> U36(isNat(x32:S)), id: 18, possubterms: U35(tt,x32:S)->[], tt->[1]) 0.003/0.003 (rule: U36(tt) -> tt, id: 19, possubterms: U36(tt)->[], tt->[1]) 0.003/0.003 (rule: U41(tt,x33:S) -> U42(isNatKind(x33:S)), id: 20, possubterms: U41(tt,x33:S)->[], tt->[1]) 0.003/0.003 (rule: U42(tt) -> tt, id: 21, possubterms: U42(tt)->[], tt->[1]) 0.003/0.003 (rule: U51(tt) -> tt, id: 22, possubterms: U51(tt)->[], tt->[1]) 0.003/0.003 (rule: U61(tt,x34:S) -> U62(isNatKind(x34:S)), id: 23, possubterms: U61(tt,x34:S)->[], tt->[1]) 0.003/0.003 (rule: U62(tt) -> tt, id: 24, possubterms: U62(tt)->[], tt->[1]) 0.003/0.003 (rule: U71(tt,x35:S) -> U72(isNatKind(x35:S),x35:S), id: 25, possubterms: U71(tt,x35:S)->[], tt->[1]) 0.003/0.003 (rule: U72(tt,x36:S) -> x36:S, id: 26, possubterms: U72(tt,x36:S)->[], tt->[1]) 0.003/0.003 (rule: U81(tt,x37:S,x38:S) -> U82(isNatKind(x37:S),x37:S,x38:S), id: 27, possubterms: U81(tt,x37:S,x38:S)->[], tt->[1]) 0.003/0.003 (rule: U82(tt,x39:S,x40:S) -> U83(isNat(x40:S),x39:S,x40:S), id: 28, possubterms: U82(tt,x39:S,x40:S)->[], tt->[1]) 0.003/0.003 (rule: U83(tt,x41:S,x42:S) -> U84(isNatKind(x42:S),x41:S,x42:S), id: 29, possubterms: U83(tt,x41:S,x42:S)->[], tt->[1]) 0.003/0.003 (rule: U84(tt,x43:S,x44:S) -> s(plus(x44:S,x43:S)), id: 30, possubterms: U84(tt,x43:S,x44:S)->[], tt->[1]) 0.003/0.003 (rule: U91(tt,x45:S) -> U92(isNatKind(x45:S)), id: 31, possubterms: U91(tt,x45:S)->[], tt->[1]) 0.003/0.003 (rule: U92(tt) -> 0, id: 32, possubterms: U92(tt)->[], tt->[1]) 0.003/0.003 (rule: isNat(plus(x46:S,x47:S)) -> U11(isNatKind(x46:S),x46:S,x47:S), id: 33, possubterms: isNat(plus(x46:S,x47:S))->[]) 0.003/0.003 (rule: isNat(x(x48:S,x49:S)) -> U31(isNatKind(x48:S),x48:S,x49:S), id: 34, possubterms: isNat(x(x48:S,x49:S))->[]) 0.003/0.003 (rule: isNat(0) -> tt, id: 35, possubterms: isNat(0)->[]) 0.003/0.003 (rule: isNat(s(x50:S)) -> U21(isNatKind(x50:S),x50:S), id: 36, possubterms: isNat(s(x50:S))->[]) 0.003/0.003 (rule: isNatKind(plus(x51:S,x52:S)) -> U41(isNatKind(x51:S),x52:S), id: 37, possubterms: isNatKind(plus(x51:S,x52:S))->[]) 0.003/0.003 (rule: isNatKind(x(x53:S,x54:S)) -> U61(isNatKind(x53:S),x54:S), id: 38, possubterms: isNatKind(x(x53:S,x54:S))->[]) 0.003/0.003 (rule: isNatKind(0) -> tt, id: 39, possubterms: isNatKind(0)->[]) 0.003/0.003 (rule: isNatKind(s(x55:S)) -> U51(isNatKind(x55:S)), id: 40, possubterms: isNatKind(s(x55:S))->[]) 0.003/0.003 (rule: plus(x56:S,0) -> U71(isNat(x56:S),x56:S), id: 41, possubterms: plus(x56:S,0)->[], 0->[2]) 0.003/0.003 (rule: plus(x58:S,s(x57:S)) -> U81(isNat(x57:S),x57:S,x58:S), id: 42, possubterms: plus(x58:S,s(x57:S))->[], s(x57:S)->[2]) 0.003/0.003 (rule: x(x59:S,0) -> U91(isNat(x59:S),x59:S), id: 43, possubterms: x(x59:S,0)->[], 0->[2]) 0.003/0.003 (rule: x(x61:S,s(x60:S)) -> U101(isNat(x60:S),x60:S,x61:S), id: 44, possubterms: x(x61:S,s(x60:S))->[], s(x60:S)->[2]) 0.003/0.003 0.003/0.003 -> Unifications: 0.003/0.003 0.003/0.003 0.003/0.003 -> Critical pairs info: 0.003/0.003 => Not trivial, Not overlay, NW1, N1 0.003/0.003 => Not trivial, Not overlay, NW1, N2 0.003/0.003 => Not trivial, Not overlay, NW1, N3 0.003/0.003 => Not trivial, Not overlay, NW1, N4 0.003/0.003 => Not trivial, Not overlay, NW1, N5 0.003/0.003 => Not trivial, Not overlay, NW1, N6 0.003/0.003 => Not trivial, Not overlay, NW1, N7 0.003/0.003 => Not trivial, Not overlay, NW1, N8 0.003/0.003 => Not trivial, Not overlay, NW1, N9 0.003/0.003 => Not trivial, Not overlay, NW1, N10 0.003/0.003 0.003/0.003 -> Problem conclusions: 0.003/0.003 Left linear, Not right linear, Not linear 0.003/0.003 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.003/0.003 Not Huet-Levy confluent, Not Newman confluent 0.003/0.003 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 No Convergence Brute Force Processor: 0.003/0.003 -> Rewritings: 0.003/0.003 s: U91(isNat(x(N:S,s(M:S))),x(N:S,s(M:S))) 0.003/0.003 Nodes: [0,1] 0.003/0.003 Edges: [(0,1)] 0.003/0.003 ID: 0 => ('U91(isNat(x(N:S,s(M:S))),x(N:S,s(M:S)))', D0) 0.003/0.003 ID: 1 => ('U91(U31(isNatKind(N:S),N:S,s(M:S)),x(N:S,s(M:S)))', D1, R34, P[1], S{x48:S -> N:S, x49:S -> s(M:S)}), NR: 'U31(isNatKind(N:S),N:S,s(M:S))' 0.003/0.003 t: x(U101(isNat(M:S),M:S,N:S),0) 0.003/0.003 Nodes: [0,1] 0.003/0.003 Edges: [(0,1)] 0.003/0.003 ID: 0 => ('x(U101(isNat(M:S),M:S,N:S),0)', D0) 0.003/0.003 ID: 1 => ('U91(isNat(U101(isNat(M:S),M:S,N:S)),U101(isNat(M:S),M:S,N:S))', D1, R43, P[], S{x59:S -> U101(isNat(M:S),M:S,N:S)}), NR: 'U91(isNat(U101(isNat(M:S),M:S,N:S)),U101(isNat(M:S),M:S,N:S))' 0.003/0.003 U91(isNat(x(N:S,s(M:S))),x(N:S,s(M:S))) ->* no union *<- x(U101(isNat(M:S),M:S,N:S),0) 0.003/0.003 "Not joinable" 0.003/0.003 0.003/0.003 The problem is not joinable. 0.003/0.003 0.01user 0.00system 0:00.03elapsed 69%CPU (0avgtext+0avgdata 12864maxresident)k 0.003/0.003 0inputs+0outputs (0major+1457minor)pagefaults 0swaps