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