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