YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (b) (h 1, 2) (c) (f 1) (fSNonEmpty) ) (RULES a -> a b -> h(c,a) h(a,a) -> f(c) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: CleanTRS Procedure: R was updated by simple cleaning of the TRS ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (b) (h 1, 2) (c) (f 1) (fSNonEmpty) ) (RULES b -> h(c,a) h(a,a) -> f(c) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: Linearity Procedure: Linear? YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a) (b) (h 1, 2) (c) (f 1) (fSNonEmpty) ) (RULES b -> h(c,a) h(a,a) -> f(c) ) Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: b -> h(c,a) h(a,a) -> f(c) -> Vars: -> Rlps: (rule: b -> h(c,a), id: 1, possubterms: b->[]) (rule: h(a,a) -> f(c), id: 2, possubterms: h(a,a)->[], a->[1], a->[2]) -> Unifications: -> Critical pairs info: -> Problem conclusions: Left linear, Right linear, Linear Weakly orthogonal, Almost orthogonal, Orthogonal Huet-Levy confluent, Not Newman confluent R is a TRS The problem is confluent.