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