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 v_NonEmpty:S:S M:S:S N:S:S V1:S:S V2:S:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U101 1) 0.002/0.002 (U102 1) 0.002/0.002 (U103 1) 0.002/0.002 (U104 1) 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U13 1) 0.002/0.002 (U14 1) 0.002/0.002 (U15 1) 0.002/0.002 (U16 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U23 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U33 1) 0.002/0.002 (U34 1) 0.002/0.002 (U35 1) 0.002/0.002 (U36 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U51 1) 0.002/0.002 (U61 1) 0.002/0.002 (U62 1) 0.002/0.002 (U71 1) 0.002/0.002 (U72 1) 0.002/0.002 (U81 1) 0.002/0.002 (U82 1) 0.002/0.002 (U83 1) 0.002/0.002 (U84 1) 0.002/0.002 (U91 1) 0.002/0.002 (U92 1) 0.002/0.002 (isNat 1) 0.002/0.002 (isNatKind 1) 0.002/0.002 (plus 2) 0.002/0.002 (x 2) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (num0) 0.002/0.002 (s) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U101(tt,M:S:S,N:S:S) -> U102(isNatKind(M:S:S),M:S:S,N:S:S) 0.002/0.002 U102(tt,M:S:S,N:S:S) -> U103(isNat(N:S:S),M:S:S,N:S:S) 0.002/0.002 U103(tt,M:S:S,N:S:S) -> U104(isNatKind(N:S:S),M:S:S,N:S:S) 0.002/0.002 U104(tt,M:S:S,N:S:S) -> plus(x(N:S:S,M:S:S),N:S:S) 0.002/0.002 U11(tt,V1:S:S,V2:S:S) -> U12(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 U12(tt,V1:S:S,V2:S:S) -> U13(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U13(tt,V1:S:S,V2:S:S) -> U14(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U14(tt,V1:S:S,V2:S:S) -> U15(isNat(V1:S:S),V2:S:S) 0.002/0.002 U15(tt,V2:S:S) -> U16(isNat(V2:S:S)) 0.002/0.002 U16(tt) -> tt 0.002/0.002 U21(tt,V1:S:S) -> U22(isNatKind(V1:S:S),V1:S:S) 0.002/0.002 U22(tt,V1:S:S) -> U23(isNat(V1:S:S)) 0.002/0.002 U23(tt) -> tt 0.002/0.002 U31(tt,V1:S:S,V2:S:S) -> U32(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 U32(tt,V1:S:S,V2:S:S) -> U33(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U33(tt,V1:S:S,V2:S:S) -> U34(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U34(tt,V1:S:S,V2:S:S) -> U35(isNat(V1:S:S),V2:S:S) 0.002/0.002 U35(tt,V2:S:S) -> U36(isNat(V2:S:S)) 0.002/0.002 U36(tt) -> tt 0.002/0.002 U41(tt,V2:S:S) -> U42(isNatKind(V2:S:S)) 0.002/0.002 U42(tt) -> tt 0.002/0.002 U51(tt) -> tt 0.002/0.002 U61(tt,V2:S:S) -> U62(isNatKind(V2:S:S)) 0.002/0.002 U62(tt) -> tt 0.002/0.002 U71(tt,N:S:S) -> U72(isNatKind(N:S:S),N:S:S) 0.002/0.002 U72(tt,N:S:S) -> N:S:S 0.002/0.002 U81(tt,M:S:S,N:S:S) -> U82(isNatKind(M:S:S),M:S:S,N:S:S) 0.002/0.002 U82(tt,M:S:S,N:S:S) -> U83(isNat(N:S:S),M:S:S,N:S:S) 0.002/0.002 U83(tt,M:S:S,N:S:S) -> U84(isNatKind(N:S:S),M:S:S,N:S:S) 0.002/0.002 U84(tt,M:S:S,N:S:S) -> s(plus(N:S:S,M:S:S)) 0.002/0.002 U91(tt,N:S:S) -> U92(isNatKind(N:S:S)) 0.002/0.002 U92(tt) -> num0 0.002/0.002 isNat(plus(V1:S:S,V2:S:S)) -> U11(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 isNat(x(V1:S:S,V2:S:S)) -> U31(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 isNat(num0) -> tt 0.002/0.002 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.002/0.002 isNatKind(plus(V1:S:S,V2:S:S)) -> U41(isNatKind(V1:S:S),V2:S:S) 0.002/0.002 isNatKind(x(V1:S:S,V2:S:S)) -> U61(isNatKind(V1:S:S),V2:S:S) 0.002/0.002 isNatKind(num0) -> tt 0.002/0.002 isNatKind(s(V1:S:S)) -> U51(isNatKind(V1:S:S)) 0.002/0.002 plus(N:S:S,num0) -> U71(isNat(N:S:S),N:S:S) 0.002/0.002 plus(N:S:S,s(M:S:S)) -> U81(isNat(M:S:S),M:S:S,N:S:S) 0.002/0.002 x(N:S:S,num0) -> U91(isNat(N:S:S),N:S:S) 0.002/0.002 x(N:S:S,s(M:S:S)) -> U101(isNat(M:S:S),M:S:S,N:S: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 v_NonEmpty:S:S M:S:S N:S:S V1:S:S V2:S:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U101 1) 0.002/0.002 (U102 1) 0.002/0.002 (U103 1) 0.002/0.002 (U104 1) 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U13 1) 0.002/0.002 (U14 1) 0.002/0.002 (U15 1) 0.002/0.002 (U16 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U23 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U33 1) 0.002/0.002 (U34 1) 0.002/0.002 (U35 1) 0.002/0.002 (U36 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U51 1) 0.002/0.002 (U61 1) 0.002/0.002 (U62 1) 0.002/0.002 (U71 1) 0.002/0.002 (U72 1) 0.002/0.002 (U81 1) 0.002/0.002 (U82 1) 0.002/0.002 (U83 1) 0.002/0.002 (U84 1) 0.002/0.002 (U91 1) 0.002/0.002 (U92 1) 0.002/0.002 (isNat 1) 0.002/0.002 (isNatKind 1) 0.002/0.002 (plus 2) 0.002/0.002 (x 2) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (num0) 0.002/0.002 (s) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U101(tt,M:S:S,N:S:S) -> U102(isNatKind(M:S:S),M:S:S,N:S:S) 0.002/0.002 U102(tt,M:S:S,N:S:S) -> U103(isNat(N:S:S),M:S:S,N:S:S) 0.002/0.002 U103(tt,M:S:S,N:S:S) -> U104(isNatKind(N:S:S),M:S:S,N:S:S) 0.002/0.002 U104(tt,M:S:S,N:S:S) -> plus(x(N:S:S,M:S:S),N:S:S) 0.002/0.002 U11(tt,V1:S:S,V2:S:S) -> U12(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 U12(tt,V1:S:S,V2:S:S) -> U13(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U13(tt,V1:S:S,V2:S:S) -> U14(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U14(tt,V1:S:S,V2:S:S) -> U15(isNat(V1:S:S),V2:S:S) 0.002/0.002 U15(tt,V2:S:S) -> U16(isNat(V2:S:S)) 0.002/0.002 U16(tt) -> tt 0.002/0.002 U21(tt,V1:S:S) -> U22(isNatKind(V1:S:S),V1:S:S) 0.002/0.002 U22(tt,V1:S:S) -> U23(isNat(V1:S:S)) 0.002/0.002 U23(tt) -> tt 0.002/0.002 U31(tt,V1:S:S,V2:S:S) -> U32(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 U32(tt,V1:S:S,V2:S:S) -> U33(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U33(tt,V1:S:S,V2:S:S) -> U34(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U34(tt,V1:S:S,V2:S:S) -> U35(isNat(V1:S:S),V2:S:S) 0.002/0.002 U35(tt,V2:S:S) -> U36(isNat(V2:S:S)) 0.002/0.002 U36(tt) -> tt 0.002/0.002 U41(tt,V2:S:S) -> U42(isNatKind(V2:S:S)) 0.002/0.002 U42(tt) -> tt 0.002/0.002 U51(tt) -> tt 0.002/0.002 U61(tt,V2:S:S) -> U62(isNatKind(V2:S:S)) 0.002/0.002 U62(tt) -> tt 0.002/0.002 U71(tt,N:S:S) -> U72(isNatKind(N:S:S),N:S:S) 0.002/0.002 U72(tt,N:S:S) -> N:S:S 0.002/0.002 U81(tt,M:S:S,N:S:S) -> U82(isNatKind(M:S:S),M:S:S,N:S:S) 0.002/0.002 U82(tt,M:S:S,N:S:S) -> U83(isNat(N:S:S),M:S:S,N:S:S) 0.002/0.002 U83(tt,M:S:S,N:S:S) -> U84(isNatKind(N:S:S),M:S:S,N:S:S) 0.002/0.002 U84(tt,M:S:S,N:S:S) -> s(plus(N:S:S,M:S:S)) 0.002/0.002 U91(tt,N:S:S) -> U92(isNatKind(N:S:S)) 0.002/0.002 U92(tt) -> num0 0.002/0.002 isNat(plus(V1:S:S,V2:S:S)) -> U11(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 isNat(x(V1:S:S,V2:S:S)) -> U31(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 isNat(num0) -> tt 0.002/0.002 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.002/0.002 isNatKind(plus(V1:S:S,V2:S:S)) -> U41(isNatKind(V1:S:S),V2:S:S) 0.002/0.002 isNatKind(x(V1:S:S,V2:S:S)) -> U61(isNatKind(V1:S:S),V2:S:S) 0.002/0.002 isNatKind(num0) -> tt 0.002/0.002 isNatKind(s(V1:S:S)) -> U51(isNatKind(V1:S:S)) 0.002/0.002 plus(N:S:S,num0) -> U71(isNat(N:S:S),N:S:S) 0.002/0.002 plus(N:S:S,s(M:S:S)) -> U81(isNat(M:S:S),M:S:S,N:S:S) 0.002/0.002 x(N:S:S,num0) -> U91(isNat(N:S:S),N:S:S) 0.002/0.002 x(N:S:S,s(M:S:S)) -> U101(isNat(M:S:S),M:S:S,N:S: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 v_NonEmpty:S:S M:S:S N:S:S V1:S:S V2:S:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U101 1) 0.002/0.002 (U102 1) 0.002/0.002 (U103 1) 0.002/0.002 (U104 1) 0.002/0.002 (U11 1) 0.002/0.002 (U12 1) 0.002/0.002 (U13 1) 0.002/0.002 (U14 1) 0.002/0.002 (U15 1) 0.002/0.002 (U16 1) 0.002/0.002 (U21 1) 0.002/0.002 (U22 1) 0.002/0.002 (U23 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U33 1) 0.002/0.002 (U34 1) 0.002/0.002 (U35 1) 0.002/0.002 (U36 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U51 1) 0.002/0.002 (U61 1) 0.002/0.002 (U62 1) 0.002/0.002 (U71 1) 0.002/0.002 (U72 1) 0.002/0.002 (U81 1) 0.002/0.002 (U82 1) 0.002/0.002 (U83 1) 0.002/0.002 (U84 1) 0.002/0.002 (U91 1) 0.002/0.002 (U92 1) 0.002/0.002 (isNat 1) 0.002/0.002 (isNatKind 1) 0.002/0.002 (plus 2) 0.002/0.002 (x 2) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (num0) 0.002/0.002 (s) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U101(tt,M:S:S,N:S:S) -> U102(isNatKind(M:S:S),M:S:S,N:S:S) 0.002/0.002 U102(tt,M:S:S,N:S:S) -> U103(isNat(N:S:S),M:S:S,N:S:S) 0.002/0.002 U103(tt,M:S:S,N:S:S) -> U104(isNatKind(N:S:S),M:S:S,N:S:S) 0.002/0.002 U104(tt,M:S:S,N:S:S) -> plus(x(N:S:S,M:S:S),N:S:S) 0.002/0.002 U11(tt,V1:S:S,V2:S:S) -> U12(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 U12(tt,V1:S:S,V2:S:S) -> U13(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U13(tt,V1:S:S,V2:S:S) -> U14(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U14(tt,V1:S:S,V2:S:S) -> U15(isNat(V1:S:S),V2:S:S) 0.002/0.002 U15(tt,V2:S:S) -> U16(isNat(V2:S:S)) 0.002/0.002 U16(tt) -> tt 0.002/0.002 U21(tt,V1:S:S) -> U22(isNatKind(V1:S:S),V1:S:S) 0.002/0.002 U22(tt,V1:S:S) -> U23(isNat(V1:S:S)) 0.002/0.002 U23(tt) -> tt 0.002/0.002 U31(tt,V1:S:S,V2:S:S) -> U32(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 U32(tt,V1:S:S,V2:S:S) -> U33(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U33(tt,V1:S:S,V2:S:S) -> U34(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U34(tt,V1:S:S,V2:S:S) -> U35(isNat(V1:S:S),V2:S:S) 0.002/0.002 U35(tt,V2:S:S) -> U36(isNat(V2:S:S)) 0.002/0.002 U36(tt) -> tt 0.002/0.002 U41(tt,V2:S:S) -> U42(isNatKind(V2:S:S)) 0.002/0.002 U42(tt) -> tt 0.002/0.002 U51(tt) -> tt 0.002/0.002 U61(tt,V2:S:S) -> U62(isNatKind(V2:S:S)) 0.002/0.002 U62(tt) -> tt 0.002/0.002 U71(tt,N:S:S) -> U72(isNatKind(N:S:S),N:S:S) 0.002/0.002 U72(tt,N:S:S) -> N:S:S 0.002/0.002 U81(tt,M:S:S,N:S:S) -> U82(isNatKind(M:S:S),M:S:S,N:S:S) 0.002/0.002 U82(tt,M:S:S,N:S:S) -> U83(isNat(N:S:S),M:S:S,N:S:S) 0.002/0.002 U83(tt,M:S:S,N:S:S) -> U84(isNatKind(N:S:S),M:S:S,N:S:S) 0.002/0.002 U84(tt,M:S:S,N:S:S) -> s(plus(N:S:S,M:S:S)) 0.002/0.002 U91(tt,N:S:S) -> U92(isNatKind(N:S:S)) 0.002/0.002 U92(tt) -> num0 0.002/0.002 isNat(plus(V1:S:S,V2:S:S)) -> U11(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 isNat(x(V1:S:S,V2:S:S)) -> U31(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 isNat(num0) -> tt 0.002/0.002 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.002/0.002 isNatKind(plus(V1:S:S,V2:S:S)) -> U41(isNatKind(V1:S:S),V2:S:S) 0.002/0.002 isNatKind(x(V1:S:S,V2:S:S)) -> U61(isNatKind(V1:S:S),V2:S:S) 0.002/0.002 isNatKind(num0) -> tt 0.002/0.002 isNatKind(s(V1:S:S)) -> U51(isNatKind(V1:S:S)) 0.002/0.002 plus(N:S:S,num0) -> U71(isNat(N:S:S),N:S:S) 0.002/0.002 plus(N:S:S,s(M:S:S)) -> U81(isNat(M:S:S),M:S:S,N:S:S) 0.002/0.002 x(N:S:S,num0) -> U91(isNat(N:S:S),N:S:S) 0.002/0.002 x(N:S:S,s(M:S:S)) -> U101(isNat(M:S:S),M:S:S,N:S:S) 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 Huet Levy Processor: 0.002/0.002 -> Rules: 0.002/0.002 U101(tt,M:S:S,N:S:S) -> U102(isNatKind(M:S:S),M:S:S,N:S:S) 0.002/0.002 U102(tt,M:S:S,N:S:S) -> U103(isNat(N:S:S),M:S:S,N:S:S) 0.002/0.002 U103(tt,M:S:S,N:S:S) -> U104(isNatKind(N:S:S),M:S:S,N:S:S) 0.002/0.002 U104(tt,M:S:S,N:S:S) -> plus(x(N:S:S,M:S:S),N:S:S) 0.002/0.002 U11(tt,V1:S:S,V2:S:S) -> U12(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 U12(tt,V1:S:S,V2:S:S) -> U13(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U13(tt,V1:S:S,V2:S:S) -> U14(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U14(tt,V1:S:S,V2:S:S) -> U15(isNat(V1:S:S),V2:S:S) 0.002/0.002 U15(tt,V2:S:S) -> U16(isNat(V2:S:S)) 0.002/0.002 U16(tt) -> tt 0.002/0.002 U21(tt,V1:S:S) -> U22(isNatKind(V1:S:S),V1:S:S) 0.002/0.002 U22(tt,V1:S:S) -> U23(isNat(V1:S:S)) 0.002/0.002 U23(tt) -> tt 0.002/0.002 U31(tt,V1:S:S,V2:S:S) -> U32(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 U32(tt,V1:S:S,V2:S:S) -> U33(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U33(tt,V1:S:S,V2:S:S) -> U34(isNatKind(V2:S:S),V1:S:S,V2:S:S) 0.002/0.002 U34(tt,V1:S:S,V2:S:S) -> U35(isNat(V1:S:S),V2:S:S) 0.002/0.002 U35(tt,V2:S:S) -> U36(isNat(V2:S:S)) 0.002/0.002 U36(tt) -> tt 0.002/0.002 U41(tt,V2:S:S) -> U42(isNatKind(V2:S:S)) 0.002/0.002 U42(tt) -> tt 0.002/0.002 U51(tt) -> tt 0.002/0.002 U61(tt,V2:S:S) -> U62(isNatKind(V2:S:S)) 0.002/0.002 U62(tt) -> tt 0.002/0.002 U71(tt,N:S:S) -> U72(isNatKind(N:S:S),N:S:S) 0.002/0.002 U72(tt,N:S:S) -> N:S:S 0.002/0.002 U81(tt,M:S:S,N:S:S) -> U82(isNatKind(M:S:S),M:S:S,N:S:S) 0.002/0.002 U82(tt,M:S:S,N:S:S) -> U83(isNat(N:S:S),M:S:S,N:S:S) 0.002/0.002 U83(tt,M:S:S,N:S:S) -> U84(isNatKind(N:S:S),M:S:S,N:S:S) 0.002/0.002 U84(tt,M:S:S,N:S:S) -> s(plus(N:S:S,M:S:S)) 0.002/0.002 U91(tt,N:S:S) -> U92(isNatKind(N:S:S)) 0.002/0.002 U92(tt) -> num0 0.002/0.002 isNat(plus(V1:S:S,V2:S:S)) -> U11(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 isNat(x(V1:S:S,V2:S:S)) -> U31(isNatKind(V1:S:S),V1:S:S,V2:S:S) 0.002/0.002 isNat(num0) -> tt 0.002/0.002 isNat(s(V1:S:S)) -> U21(isNatKind(V1:S:S),V1:S:S) 0.002/0.002 isNatKind(plus(V1:S:S,V2:S:S)) -> U41(isNatKind(V1:S:S),V2:S:S) 0.002/0.002 isNatKind(x(V1:S:S,V2:S:S)) -> U61(isNatKind(V1:S:S),V2:S:S) 0.002/0.002 isNatKind(num0) -> tt 0.002/0.002 isNatKind(s(V1:S:S)) -> U51(isNatKind(V1:S:S)) 0.002/0.002 plus(N:S:S,num0) -> U71(isNat(N:S:S),N:S:S) 0.002/0.002 plus(N:S:S,s(M:S:S)) -> U81(isNat(M:S:S),M:S:S,N:S:S) 0.002/0.002 x(N:S:S,num0) -> U91(isNat(N:S:S),N:S:S) 0.002/0.002 x(N:S:S,s(M:S:S)) -> U101(isNat(M:S:S),M:S:S,N:S:S) 0.002/0.002 -> Vars: 0.002/0.002 M:S, N:S, M:S, N:S, M:S, N:S, M:S, N:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V2:S, V1:S, V1:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V2:S, V2:S, V2:S, N:S, N:S, M:S, N:S, M:S, N:S, M:S, N:S, M:S, N:S, N:S, V1:S, V2:S, V1:S, V2:S, V1:S, V1:S, V2:S, V1:S, V2:S, V1:S, N:S, M:S, N:S, N:S, M:S, N:S 0.002/0.002 -> UVars: 0.002/0.002 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [M:S], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.002/0.002 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.002/0.002 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.002/0.002 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.002/0.002 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.002/0.002 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.002/0.002 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.002/0.002 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.002/0.002 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.002/0.002 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.002/0.002 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.002/0.002 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 24, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.002/0.002 (UV-RuleId: 26, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 27, UV-LActive: [], UV-RActive: [M:S], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.002/0.002 (UV-RuleId: 28, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.002/0.002 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.002/0.002 (UV-RuleId: 30, UV-LActive: [], UV-RActive: [], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.002/0.002 (UV-RuleId: 31, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 32, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 33, UV-LActive: [V2:S], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S, V2:S]) 0.002/0.002 (UV-RuleId: 34, UV-LActive: [V2:S], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S, V2:S]) 0.002/0.002 (UV-RuleId: 35, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.002/0.002 (UV-RuleId: 37, UV-LActive: [V2:S], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 38, UV-LActive: [V2:S], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 39, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 40, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 41, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.002/0.002 (UV-RuleId: 42, UV-LActive: [], UV-RActive: [M:S], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 0.002/0.002 (UV-RuleId: 43, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.002/0.002 (UV-RuleId: 44, UV-LActive: [], UV-RActive: [M:S], UV-LFrozen: [M:S, N:S], UV-RFrozen: [M:S, N:S]) 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, 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, x62 0.002/0.002 -> PVars: 0.002/0.002 M:S: [x6, x8, x10, x12, x38, x40, x42, x44, x58, x61], N:S: [x7, x9, x11, x13, x36, x37, x39, x41, x43, x45, x46, x57, x59, x60, x62], V1:S: [x14, x16, x18, x20, x23, x24, x25, x27, x29, x31, x47, x49, x51, x52, x54, x56], V2:S: [x15, x17, x19, x21, x22, x26, x28, x30, x32, x33, x34, x35, x48, x50, x53, x55] 0.002/0.002 0.002/0.002 -> Rlps: 0.002/0.002 (rule: U101(tt,x6:S,x7:S) -> U102(isNatKind(x6:S),x6:S,x7:S), id: 1, possubterms: U101(tt,x6:S,x7:S)->[], tt->[1]) 0.002/0.002 (rule: U102(tt,x8:S,x9:S) -> U103(isNat(x9:S),x8:S,x9:S), id: 2, possubterms: U102(tt,x8:S,x9:S)->[], tt->[1]) 0.002/0.002 (rule: U103(tt,x10:S,x11:S) -> U104(isNatKind(x11:S),x10:S,x11:S), id: 3, possubterms: U103(tt,x10:S,x11:S)->[], tt->[1]) 0.002/0.002 (rule: U104(tt,x12:S,x13:S) -> plus(x(x13:S,x12:S),x13:S), id: 4, possubterms: U104(tt,x12:S,x13:S)->[], tt->[1]) 0.002/0.002 (rule: U11(tt,x14:S,x15:S) -> U12(isNatKind(x14:S),x14:S,x15:S), id: 5, possubterms: U11(tt,x14:S,x15:S)->[], tt->[1]) 0.002/0.002 (rule: U12(tt,x16:S,x17:S) -> U13(isNatKind(x17:S),x16:S,x17:S), id: 6, possubterms: U12(tt,x16:S,x17:S)->[], tt->[1]) 0.002/0.002 (rule: U13(tt,x18:S,x19:S) -> U14(isNatKind(x19:S),x18:S,x19:S), id: 7, possubterms: U13(tt,x18:S,x19:S)->[], tt->[1]) 0.002/0.002 (rule: U14(tt,x20:S,x21:S) -> U15(isNat(x20:S),x21:S), id: 8, possubterms: U14(tt,x20:S,x21:S)->[], tt->[1]) 0.002/0.002 (rule: U15(tt,x22:S) -> U16(isNat(x22:S)), id: 9, possubterms: U15(tt,x22:S)->[], tt->[1]) 0.002/0.002 (rule: U16(tt) -> tt, id: 10, possubterms: U16(tt)->[], tt->[1]) 0.002/0.002 (rule: U21(tt,x23:S) -> U22(isNatKind(x23:S),x23:S), id: 11, possubterms: U21(tt,x23:S)->[], tt->[1]) 0.002/0.002 (rule: U22(tt,x24:S) -> U23(isNat(x24:S)), id: 12, possubterms: U22(tt,x24:S)->[], tt->[1]) 0.002/0.002 (rule: U23(tt) -> tt, id: 13, possubterms: U23(tt)->[], tt->[1]) 0.002/0.002 (rule: U31(tt,x25:S,x26:S) -> U32(isNatKind(x25:S),x25:S,x26:S), id: 14, possubterms: U31(tt,x25:S,x26:S)->[], tt->[1]) 0.002/0.002 (rule: U32(tt,x27:S,x28:S) -> U33(isNatKind(x28:S),x27:S,x28:S), id: 15, possubterms: U32(tt,x27:S,x28:S)->[], tt->[1]) 0.002/0.002 (rule: U33(tt,x29:S,x30:S) -> U34(isNatKind(x30:S),x29:S,x30:S), id: 16, possubterms: U33(tt,x29:S,x30:S)->[], tt->[1]) 0.002/0.002 (rule: U34(tt,x31:S,x32:S) -> U35(isNat(x31:S),x32:S), id: 17, possubterms: U34(tt,x31:S,x32:S)->[], tt->[1]) 0.002/0.002 (rule: U35(tt,x33:S) -> U36(isNat(x33:S)), id: 18, possubterms: U35(tt,x33:S)->[], tt->[1]) 0.002/0.002 (rule: U36(tt) -> tt, id: 19, possubterms: U36(tt)->[], tt->[1]) 0.002/0.002 (rule: U41(tt,x34:S) -> U42(isNatKind(x34:S)), id: 20, possubterms: U41(tt,x34:S)->[], tt->[1]) 0.002/0.002 (rule: U42(tt) -> tt, id: 21, possubterms: U42(tt)->[], tt->[1]) 0.002/0.002 (rule: U51(tt) -> tt, id: 22, possubterms: U51(tt)->[], tt->[1]) 0.002/0.002 (rule: U61(tt,x35:S) -> U62(isNatKind(x35:S)), id: 23, possubterms: U61(tt,x35:S)->[], tt->[1]) 0.002/0.002 (rule: U62(tt) -> tt, id: 24, possubterms: U62(tt)->[], tt->[1]) 0.002/0.002 (rule: U71(tt,x36:S) -> U72(isNatKind(x36:S),x36:S), id: 25, possubterms: U71(tt,x36:S)->[], tt->[1]) 0.002/0.002 (rule: U72(tt,x37:S) -> x37:S, id: 26, possubterms: U72(tt,x37:S)->[], tt->[1]) 0.002/0.002 (rule: U81(tt,x38:S,x39:S) -> U82(isNatKind(x38:S),x38:S,x39:S), id: 27, possubterms: U81(tt,x38:S,x39:S)->[], tt->[1]) 0.002/0.002 (rule: U82(tt,x40:S,x41:S) -> U83(isNat(x41:S),x40:S,x41:S), id: 28, possubterms: U82(tt,x40:S,x41:S)->[], tt->[1]) 0.002/0.002 (rule: U83(tt,x42:S,x43:S) -> U84(isNatKind(x43:S),x42:S,x43:S), id: 29, possubterms: U83(tt,x42:S,x43:S)->[], tt->[1]) 0.002/0.002 (rule: U84(tt,x44:S,x45:S) -> s(plus(x45:S,x44:S)), id: 30, possubterms: U84(tt,x44:S,x45:S)->[], tt->[1]) 0.002/0.002 (rule: U91(tt,x46:S) -> U92(isNatKind(x46:S)), id: 31, possubterms: U91(tt,x46:S)->[], tt->[1]) 0.002/0.002 (rule: U92(tt) -> num0, id: 32, possubterms: U92(tt)->[], tt->[1]) 0.002/0.002 (rule: isNat(plus(x47:S,x48:S)) -> U11(isNatKind(x47:S),x47:S,x48:S), id: 33, possubterms: isNat(plus(x47:S,x48:S))->[], plus(x47:S,x48:S)->[1]) 0.002/0.002 (rule: isNat(x(x49:S,x50:S)) -> U31(isNatKind(x49:S),x49:S,x50:S), id: 34, possubterms: isNat(x(x49:S,x50:S))->[], x(x49:S,x50:S)->[1]) 0.002/0.002 (rule: isNat(num0) -> tt, id: 35, possubterms: isNat(num0)->[], num0->[1]) 0.002/0.002 (rule: isNat(s(x51:S)) -> U21(isNatKind(x51:S),x51:S), id: 36, possubterms: isNat(s(x51:S))->[], s(x51:S)->[1]) 0.002/0.002 (rule: isNatKind(plus(x52:S,x53:S)) -> U41(isNatKind(x52:S),x53:S), id: 37, possubterms: isNatKind(plus(x52:S,x53:S))->[], plus(x52:S,x53:S)->[1]) 0.002/0.002 (rule: isNatKind(x(x54:S,x55:S)) -> U61(isNatKind(x54:S),x55:S), id: 38, possubterms: isNatKind(x(x54:S,x55:S))->[], x(x54:S,x55:S)->[1]) 0.002/0.002 (rule: isNatKind(num0) -> tt, id: 39, possubterms: isNatKind(num0)->[], num0->[1]) 0.002/0.002 (rule: isNatKind(s(x56:S)) -> U51(isNatKind(x56:S)), id: 40, possubterms: isNatKind(s(x56:S))->[], s(x56:S)->[1]) 0.002/0.002 (rule: plus(x57:S,num0) -> U71(isNat(x57:S),x57:S), id: 41, possubterms: plus(x57:S,num0)->[], num0->[2]) 0.002/0.002 (rule: plus(x59:S,s(x58:S)) -> U81(isNat(x58:S),x58:S,x59:S), id: 42, possubterms: plus(x59:S,s(x58:S))->[], s(x58:S)->[2]) 0.002/0.002 (rule: x(x60:S,num0) -> U91(isNat(x60:S),x60:S), id: 43, possubterms: x(x60:S,num0)->[], num0->[2]) 0.002/0.002 (rule: x(x62:S,s(x61:S)) -> U101(isNat(x61:S),x61:S,x62:S), id: 44, possubterms: x(x62:S,s(x61:S))->[], s(x61:S)->[2]) 0.002/0.002 0.002/0.002 -> Unifications: 0.002/0.002 (R33 unifies with R41 at p: [1], l: isNat(plus(x47:S,x48:S)), lp: plus(x47:S,x48:S), sig: {x47:S -> N:S:S,x48:S -> num0}, l': plus(N:S:S,num0), r: U11(isNatKind(x47:S),x47:S,x48:S), r': U71(isNat(N:S:S),N:S:S)) 0.002/0.002 (R33 unifies with R42 at p: [1], l: isNat(plus(x47:S,x48:S)), lp: plus(x47:S,x48:S), sig: {x47:S -> N:S:S,x48:S -> s(M:S:S)}, l': plus(N:S:S,s(M:S:S)), r: U11(isNatKind(x47:S),x47:S,x48:S), r': U81(isNat(M:S:S),M:S:S,N:S:S)) 0.002/0.002 (R34 unifies with R43 at p: [1], l: isNat(x(x49:S,x50:S)), lp: x(x49:S,x50:S), sig: {x49:S -> N:S:S,x50:S -> num0}, l': x(N:S:S,num0), r: U31(isNatKind(x49:S),x49:S,x50:S), r': U91(isNat(N:S:S),N:S:S)) 0.002/0.002 (R34 unifies with R44 at p: [1], l: isNat(x(x49:S,x50:S)), lp: x(x49:S,x50:S), sig: {x49:S -> N:S:S,x50:S -> s(M:S:S)}, l': x(N:S:S,s(M:S:S)), r: U31(isNatKind(x49:S),x49:S,x50:S), r': U101(isNat(M:S:S),M:S:S,N:S:S)) 0.002/0.002 (R37 unifies with R41 at p: [1], l: isNatKind(plus(x52:S,x53:S)), lp: plus(x52:S,x53:S), sig: {x52:S -> N:S:S,x53:S -> num0}, l': plus(N:S:S,num0), r: U41(isNatKind(x52:S),x53:S), r': U71(isNat(N:S:S),N:S:S)) 0.002/0.002 (R37 unifies with R42 at p: [1], l: isNatKind(plus(x52:S,x53:S)), lp: plus(x52:S,x53:S), sig: {x52:S -> N:S:S,x53:S -> s(M:S:S)}, l': plus(N:S:S,s(M:S:S)), r: U41(isNatKind(x52:S),x53:S), r': U81(isNat(M:S:S),M:S:S,N:S:S)) 0.002/0.002 (R38 unifies with R43 at p: [1], l: isNatKind(x(x54:S,x55:S)), lp: x(x54:S,x55:S), sig: {x54:S -> N:S:S,x55:S -> num0}, l': x(N:S:S,num0), r: U61(isNatKind(x54:S),x55:S), r': U91(isNat(N:S:S),N:S:S)) 0.002/0.002 (R38 unifies with R44 at p: [1], l: isNatKind(x(x54:S,x55:S)), lp: x(x54:S,x55:S), sig: {x54:S -> N:S:S,x55:S -> s(M:S:S)}, l': x(N:S:S,s(M:S:S)), r: U61(isNatKind(x54:S),x55:S), r': U101(isNat(M:S:S),M:S:S,N:S:S)) 0.002/0.002 0.002/0.002 -> Critical pairs info: 0.002/0.002 => Not trivial, Not overlay, NW0, N1 0.002/0.002 => Not trivial, Not overlay, NW0, N2 0.002/0.002 => Not trivial, Not overlay, NW0, N3 0.002/0.002 => Not trivial, Not overlay, NW0, N4 0.002/0.002 => Not trivial, Not overlay, NW0, N5 0.002/0.002 => Not trivial, Not overlay, NW0, N6 0.002/0.002 => Not trivial, Not overlay, NW0, N7 0.002/0.002 => Not trivial, Not overlay, NW0, N8 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 Different Normal CP Terms Processor: 0.002/0.002 => Not trivial, Not overlay, NW0, N1, Normal and not trivial cp 0.002/0.002 0.002/0.002 The problem is not joinable. 0.002/0.002 0.01user 0.00system 0:00.02elapsed 65%CPU (0avgtext+0avgdata 11864maxresident)k 0.002/0.002 8inputs+0outputs (0major+1172minor)pagefaults 0swaps