(ignored inputs)COMMENT doi:10.1145/322217.322230 [12] p. 814 , attributed to Levy submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama Rewrite Rules: [ F(A,A) -> G(B,B), A -> A', F(A',?x) -> F(?x,?x), F(?x,A') -> F(?x,?x), G(B,B) -> F(A,A), B -> B', G(B',?x) -> G(?x,?x), G(?x,B') -> G(?x,?x) ] Apply Direct Methods... Inner CPs: [ F(A',A) = G(B,B), F(A,A') = G(B,B), G(B',B) = F(A,A), G(B,B') = F(A,A) ] Outer CPs: [ F(A',A') = F(A',A'), G(B',B') = G(B',B') ] not Overlay, check Termination... unknown/not Terminating unknown Knuth & Bendix Left-Linear, not Right-Linear unknown Development Closed unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow inner CP cond (upside-parallel) innter CP Cond (outside) unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: [ F(A,A') = G(B,B) {}, F(A',A) = G(B,B) {}, F(A',A') = G(B,B) {}, G(B,B') = F(A,A) {}, G(B',B) = F(A,A) {}, G(B',B') = F(A,A) {} ] unknown Toyama (Parallel CPs) Simultaneous CPs: [ F(A',A') = G(B,B), F(A',A) = G(B,B), F(A,A') = G(B,B), G(B,B) = F(A',A), G(B,B) = F(A,A'), F(A',A') = F(A',A'), G(B',B') = F(A,A), G(B',B) = F(A,A), G(B,B') = F(A,A), F(A,A) = G(B',B), F(A,A) = G(B,B'), G(B',B') = G(B',B') ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair by Rules <1, 0> preceded by [(F,1)] joinable by a reduction of rules <[([],2)], [([],4)]> Critical Pair by Rules <1, 0> preceded by [(F,2)] joinable by a reduction of rules <[([],3)], [([],4)]> Critical Pair by Rules <5, 4> preceded by [(G,1)] joinable by a reduction of rules <[([],6)], [([],0)]> Critical Pair by Rules <5, 4> preceded by [(G,2)] joinable by a reduction of rules <[([],7)], [([],0)]> Critical Pair by Rules <3, 2> preceded by [] joinable by a reduction of rules <[], []> Critical Pair by Rules <7, 6> preceded by [] joinable by a reduction of rules <[], []> unknown Diagram Decreasing [ F(A,A) -> G(B,B), A -> A', F(A',?x) -> F(?x,?x), F(?x_1,A') -> F(?x_1,?x_1), G(B,B) -> F(A,A), B -> B', G(B',?x_2) -> G(?x_2,?x_2), G(?x_3,B') -> G(?x_3,?x_3) ] Sort Assignment: A : =>21 B : =>17 F : 21*21=>15 G : 17*17=>15 A' : =>21 B' : =>17 non-linear variables: {?x,?x_1,?x_2,?x_3} non-linear types: {21,17} types leq non-linear types: {21,17} rules applicable to terms of non-linear types: [ A -> A', B -> B' ] Rnl: 0: {} 1: {} 2: {1} 3: {1} 4: {} 5: {} 6: {5} 7: {5} terms of non-linear types are innermost terminating Critical Pair by Rules <1, 0> convertible by a reduction of rules [->(2),->(0)] convertible by a reduction of rules [->(2),(4)<-] convertible by a reduction of rules [(1)<-,(4)<-] convertible by a reduction of rules [->(1),(1)<-,->(3),->(0)] Critical Pair by Rules <1, 0> convertible by a reduction of rules [->(3),->(0)] convertible by a reduction of rules [->(3),(4)<-] convertible by a reduction of rules [(1)<-,(4)<-] convertible by a reduction of rules [->(1),(1)<-,->(2),->(0)] Critical Pair by Rules <5, 4> convertible by a reduction of rules [->(6),->(4)] convertible by a reduction of rules [->(6),(0)<-] convertible by a reduction of rules [(5)<-,(0)<-] convertible by a reduction of rules [->(5),(5)<-,->(7),->(4)] Critical Pair by Rules <5, 4> convertible by a reduction of rules [->(7),->(4)] convertible by a reduction of rules [->(7),(0)<-] convertible by a reduction of rules [(5)<-,(0)<-] convertible by a reduction of rules [->(5),(5)<-,->(6),->(4)] Critical Pair by Rules <3, 2> convertible by a reduction of rules [] Critical Pair by Rules <7, 6> convertible by a reduction of rules [] Not Satisfiable unknown Quasi-Linear & Linearized-Decreasing [ F(A,A) -> G(B,B), A -> A', F(A',?x) -> F(?x,?x), F(?x_1,A') -> F(?x_1,?x_1), G(B,B) -> F(A,A), B -> B', G(B',?x_2) -> G(?x_2,?x_2), G(?x_3,B') -> G(?x_3,?x_3) ] Sort Assignment: A : =>21 B : =>17 F : 21*21=>15 G : 17*17=>15 A' : =>21 B' : =>17 non-linear variables: {?x,?x_1,?x_2,?x_3} non-linear types: {21,17} types leq non-linear types: {21,17} rules applicable to terms of non-linear types: [ A -> A', B -> B' ] terms of non-linear types are terminating Check Joinablility of CP from NLR: done. Critical Pair by Rules <1, 0> convertible by a reduction of rules [->(2),->(0)] convertible by a reduction of rules [->(2),(4)<-] convertible by a reduction of rules [(1)<-,(4)<-] convertible by a reduction of rules [->(1),(1)<-,->(3),->(0)] Critical Pair by Rules <1, 0> convertible by a reduction of rules [->(3),->(0)] convertible by a reduction of rules [->(3),(4)<-] convertible by a reduction of rules [(1)<-,(4)<-] convertible by a reduction of rules [->(1),(1)<-,->(2),->(0)] Critical Pair by Rules <5, 4> convertible by a reduction of rules [->(6),->(4)] convertible by a reduction of rules [->(6),(0)<-] convertible by a reduction of rules [(5)<-,(0)<-] convertible by a reduction of rules [->(5),(5)<-,->(7),->(4)] Critical Pair by Rules <5, 4> convertible by a reduction of rules [->(7),->(4)] convertible by a reduction of rules [->(7),(0)<-] convertible by a reduction of rules [(5)<-,(0)<-] convertible by a reduction of rules [->(5),(5)<-,->(6),->(4)] Critical Pair by Rules <3, 2> convertible by a reduction of rules [] Critical Pair by Rules <7, 6> convertible by a reduction of rules [] Not Satisfiable unknown Strongly Quasi-Linear & Hierarchically Decreasing check Non-Confluence... obtain 11 rules by 3 steps unfolding obtain 58 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (success) Witness for Non-Confluence: G(B',B')> Direct Methods: not CR Combined result: not CR 49.trs: Success(not CR) NO (2963 msec.)