5.89/2.84	YES
5.89/2.84	
5.89/2.84	Proof:
5.89/2.84	This system is confluent.
5.89/2.84	By \cite{GNG13}, Theorem 9.
5.89/2.84	This system is of type 3 or smaller.
5.89/2.84	This system is deterministic.
5.89/2.84	This system is weakly left-linear.
5.89/2.84	System R transformed to optimized U(R).
5.89/2.84	This system is confluent.
5.89/2.84	Call external tool:
5.89/2.84	./csi.sh
5.89/2.84	Input:
5.89/2.84	(VAR x)
5.89/2.84	(RULES
5.89/2.84	  f(x, x) -> a
5.89/2.84	  g(x) -> ?1(g(x), x)
5.89/2.84	  ?1(b, x) -> a
5.89/2.84	  a -> b
5.89/2.84	  b -> a
5.89/2.84	)
5.89/2.84	
5.89/2.84	 sorted: (order)
5.89/2.84	 0:f(x,x) -> a()
5.89/2.84	   a() -> b()
5.89/2.84	   b() -> a()
5.89/2.84	 1:g(x) -> ?1(g(x),x)
5.89/2.84	   ?1(b(),x) -> a()
5.89/2.84	   a() -> b()
5.89/2.84	   b() -> a()
6.21/2.84	 -----
6.21/2.84	 sorts
6.21/2.84	   [0>2, 0>4, 1>2, 1>3]
6.21/2.84	 sort attachment (strict)
6.21/2.84	   f : 4 x 4 -> 0
6.21/2.84	   a : 2
6.21/2.84	   g : 3 -> 1
6.21/2.84	   ?1 : 1 x 3 -> 1
6.21/2.84	   b : 2
6.21/2.84	 -----
6.21/2.84	 0:f(x,x) -> a()
6.21/2.84	   a() -> b()
6.21/2.84	   b() -> a()
6.21/2.84	   Qed (ToyamaOyamaguchi95Cor22)
6.21/2.84	 
6.21/2.84	 
6.21/2.84	 1:g(x) -> ?1(g(x),x)
6.21/2.84	   ?1(b(),x) -> a()
6.21/2.84	   a() -> b()
6.21/2.84	   b() -> a()
6.21/2.84	   Church Rosser Transformation Processor:
6.21/2.84	    strict:
6.21/2.84	     
6.21/2.84	    weak:
6.21/2.84	     
6.21/2.84	    critical peaks: 1
6.21/2.84	     ?1(a(),x) <-3|0[]- ?1(b(),x) -1|[]-> a()
6.21/2.84	    Shift Processor lab=left (dd) (force):
6.21/2.84	     strict:
6.21/2.84	      ?1(b(),x) -> ?1(a(),x)
6.21/2.84	      ?1(b(),x) -> a()
6.21/2.84	      ?1(a(),x) -> ?1(b(),x)
6.21/2.84	      ?1(b(),x) -> a()
6.21/2.85	     weak:
6.21/2.85	      g(x) -> ?1(g(x),x)
6.21/2.85	      ?1(b(),x) -> a()
6.21/2.85	      a() -> b()
6.21/2.85	      b() -> a()
6.21/2.85	     Shift Processor (ldh) lab=left (force):
6.21/2.85	      strict:
6.21/2.85	       
6.21/2.85	      weak:
6.21/2.85	       
6.21/2.85	      Rule Labeling Processor:
6.21/2.85	       strict:
6.21/2.85	        
6.21/2.85	       weak:
6.21/2.85	        
6.21/2.85	       rule labeling (right):
6.21/2.85	        g(x) -> ?1(g(x),x): 0
6.21/2.85	        ?1(b(),x) -> a(): 0
6.21/2.85	        a() -> b(): 0
6.21/2.85	        b() -> a(): 1
6.21/2.85	       Rule Labeling Processor:
6.21/2.85	        strict:
6.21/2.85	         
6.21/2.85	        weak:
6.21/2.85	         
6.21/2.85	        rule labeling (left):
6.21/2.85	         g(x) -> ?1(g(x),x): 0
6.21/2.85	         ?1(b(),x) -> a(): 0
6.21/2.85	         a() -> b(): 0
6.21/2.85	         b() -> a(): 0
6.21/2.85	        Decreasing Processor:
6.21/2.85	         The following diagrams are decreasing:
6.21/2.85	         peak:
6.21/2.85	          ?1(a(),x) <-3|0[==0,==1,=?1]- ?1(b(),x) -1|[==0,==1,>=0]-> a()
6.21/2.85	         joins (1):
6.21/2.85	          ?1(a(),x) -2|0[==0,==1,>=0]-> ?1(b(),x) -1|[==0,==1,>=0]-> a()
6.21/2.85	          
6.21/2.85	         Qed
6.21/2.85	  
6.21/2.85	
6.21/2.88	EOF