4.72/1.75	YES
4.72/1.75	
4.72/1.75	Proof:
4.72/1.75	This system is confluent.
4.72/1.75	By \cite{ALS94}, Theorem 4.1.
4.72/1.75	This system is of type 3 or smaller.
4.72/1.75	This system is strongly deterministic.
4.72/1.75	This system is quasi-decreasing.
4.72/1.75	By \cite{O02}, p. 214, Proposition 7.2.50.
4.72/1.75	This system is of type 3 or smaller.
4.72/1.75	This system is deterministic.
4.72/1.75	System R transformed to optimized U(R).
4.72/1.75	This system is terminating.
4.72/1.75	Call external tool:
4.72/1.75	./ttt2.sh
4.72/1.75	Input:
4.72/1.75	  f(x) -> ?1(a, x)
4.72/1.75	  ?1(b, x) -> c
4.72/1.75	  g(x, x) -> g(f(a), f(b))
4.72/1.75	
4.72/1.75	 Matrix Interpretation Processor: dim=3
4.72/1.75	  
4.72/1.75	  interpretation:
4.72/1.75	                 [1 0 0]     [1 0 0]  
4.72/1.75	   [g](x0, x1) = [0 0 1]x0 + [0 0 0]x1
4.72/1.75	                 [0 0 0]     [0 0 1]  ,
4.72/1.75	   
4.72/1.75	         [0]
4.72/1.75	   [c] = [0]
4.72/1.75	         [0],
4.72/1.75	   
4.72/1.75	         [0]
4.72/1.75	   [b] = [1]
4.72/1.75	         [1],
4.72/1.75	   
4.72/1.75	                  [1 1 1]     [1 0 0]  
4.72/1.75	   [?1](x0, x1) = [0 0 0]x0 + [0 0 0]x1
4.72/1.75	                  [0 0 0]     [0 0 0]  ,
4.72/1.75	   
4.72/1.75	         [0]
4.72/1.75	   [a] = [0]
4.72/1.75	         [0],
4.72/1.75	   
4.72/1.75	             [1 0 0]  
4.72/1.75	   [f](x0) = [1 0 0]x0
4.72/1.75	             [1 0 0]  
4.72/1.75	  orientation:
4.72/1.75	          [1 0 0]     [1 0 0]             
4.72/1.75	   f(x) = [1 0 0]x >= [0 0 0]x = ?1(a(),x)
4.72/1.75	          [1 0 0]     [0 0 0]             
4.72/1.75	   
4.72/1.75	               [1 0 0]    [2]    [0]      
4.72/1.75	   ?1(b(),x) = [0 0 0]x + [0] >= [0] = c()
4.72/1.75	               [0 0 0]    [0]    [0]      
4.72/1.75	   
4.72/1.75	            [2 0 0]     [0]                   
4.72/1.75	   g(x,x) = [0 0 1]x >= [0] = g(f(a()),f(b()))
4.72/1.75	            [0 0 1]     [0]                   
4.72/1.75	  problem:
4.72/1.75	   f(x) -> ?1(a(),x)
4.72/1.75	   g(x,x) -> g(f(a()),f(b()))
4.72/1.75	  DP Processor:
4.72/1.75	   DPs:
4.72/1.75	    g#(x,x) -> f#(b())
4.72/1.75	    g#(x,x) -> f#(a())
4.72/1.75	    g#(x,x) -> g#(f(a()),f(b()))
4.72/1.75	   TRS:
4.72/1.75	    f(x) -> ?1(a(),x)
4.72/1.75	    g(x,x) -> g(f(a()),f(b()))
4.72/1.75	   TDG Processor:
4.72/1.75	    DPs:
4.72/1.75	     g#(x,x) -> f#(b())
4.72/1.75	     g#(x,x) -> f#(a())
4.72/1.75	     g#(x,x) -> g#(f(a()),f(b()))
4.72/1.75	    TRS:
4.72/1.75	     f(x) -> ?1(a(),x)
4.72/1.75	     g(x,x) -> g(f(a()),f(b()))
4.72/1.75	    graph:
4.72/1.75	     g#(x,x) -> g#(f(a()),f(b())) -> g#(x,x) -> g#(f(a()),f(b()))
4.72/1.75	     g#(x,x) -> g#(f(a()),f(b())) -> g#(x,x) -> f#(a())
4.72/1.75	     g#(x,x) -> g#(f(a()),f(b())) -> g#(x,x) -> f#(b())
4.72/1.76	    SCC Processor:
4.72/1.76	     #sccs: 1
4.72/1.76	     #rules: 1
4.72/1.76	     #arcs: 3/9
4.72/1.76	     DPs:
4.72/1.76	      g#(x,x) -> g#(f(a()),f(b()))
4.72/1.76	     TRS:
4.72/1.76	      f(x) -> ?1(a(),x)
4.72/1.76	      g(x,x) -> g(f(a()),f(b()))
4.72/1.76	     Bounds Processor:
4.72/1.76	      bound: 1
4.72/1.76	      enrichment: match
4.72/1.76	      automaton:
4.72/1.76	       final states: {8,6,1}
4.72/1.76	       transitions:
4.72/1.76	        ?11(9,2) -> 3*
4.72/1.76	        ?11(9,4) -> 5*
4.72/1.76	        ?11(9,10) -> 5*
4.72/1.76	        ?11(10,2) -> 3*
4.72/1.76	        ?11(10,4) -> 5*
4.72/1.76	        ?11(10,10) -> 5*
4.72/1.76	        a1() -> 10*,4,9
4.72/1.76	        f80() -> 7*
4.72/1.76	        g{#,0}(5,3) -> 1*
4.72/1.76	        f0(10) -> 5*
4.72/1.76	        f0(2) -> 3*
4.72/1.76	        f0(4) -> 5*
4.72/1.76	        b0() -> 2*
4.72/1.76	        ?10(4,2) -> 3*
4.72/1.76	        ?10(4,4) -> 5*
4.72/1.76	        ?10(4,10) -> 5*
4.72/1.76	        ?10(10,7) -> 6*
4.72/1.76	        ?10(4,7) -> 6*
4.72/1.76	        ?10(10,2) -> 3*
4.72/1.76	        ?10(10,4) -> 5*
4.72/1.76	        ?10(10,10) -> 5*
4.72/1.76	        g0(5,3) -> 8*
4.72/1.76	      problem:
4.72/1.76	       DPs:
4.72/1.76	        
4.72/1.76	       TRS:
4.72/1.76	        f(x) -> ?1(a(),x)
4.72/1.76	        g(x,x) -> g(f(a()),f(b()))
4.72/1.76	      Qed
4.72/1.76	All 0 critical pairs are joinable.
4.72/1.76	
4.72/1.78	EOF