3.25/1.23	YES
3.25/1.23	
3.25/1.23	Problem:
3.25/1.23	f(x) -> c() <= a() = b()
3.25/1.23	g(x, x) -> g(f(a()), f(b()))
3.25/1.23	
3.25/1.23	Proof:
3.25/1.23	This system is confluent.
3.25/1.23	By \cite{ALS94}, Theorem 4.1.
3.25/1.23	This system is of type 3 or smaller.
3.25/1.23	This system is strongly deterministic.
3.25/1.23	All 0 critical pairs are joinable.
3.25/1.23	This system is quasi-decreasing.
3.25/1.23	By \cite{O02}, p. 214, Proposition 7.2.50.
3.25/1.23	This system is of type 3 or smaller.
3.25/1.23	This system is deterministic.
3.25/1.23	System R transformed to U(R).
3.25/1.23	This system is terminating.
3.25/1.23	Call external tool:
3.25/1.24	./ttt2.sh
3.25/1.24	Input:
3.25/1.24	  ?1(b(), x) -> c()
3.25/1.24	  f(x) -> ?1(a(), x)
3.25/1.24	  g(x, x) -> g(f(a()), f(b()))
3.25/1.24	
3.25/1.24	 Matrix Interpretation Processor: dim=3
3.25/1.24	  
3.25/1.24	  interpretation:
3.25/1.24	                 [1 0 0]     [1 0 0]     [0]
3.25/1.24	   [g](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
3.25/1.24	                 [0 0 0]     [0 0 1]     [1],
3.25/1.24	   
3.25/1.24	         [0]
3.25/1.24	   [a] = [0]
3.25/1.24	         [0],
3.25/1.24	   
3.25/1.24	             [1 0 0]  
3.25/1.24	   [f](x0) = [0 0 1]x0
3.25/1.24	             [0 0 0]  ,
3.25/1.24	   
3.25/1.24	         [0]
3.25/1.24	   [c] = [0]
3.25/1.24	         [0],
3.25/1.24	   
3.25/1.24	                  [1 1 1]     [1 0 0]  
3.25/1.24	   [?1](x0, x1) = [0 0 0]x0 + [0 0 0]x1
3.25/1.24	                  [0 0 0]     [0 0 0]  ,
3.25/1.24	   
3.25/1.24	         [0]
3.25/1.24	   [b] = [1]
3.25/1.24	         [1]
3.25/1.24	  orientation:
3.25/1.24	               [1 0 0]    [2]    [0]      
3.25/1.24	   ?1(b(),x) = [0 0 0]x + [0] >= [0] = c()
3.25/1.25	               [0 0 0]    [0]    [0]      
3.25/1.25	   
3.25/1.25	          [1 0 0]     [1 0 0]             
3.25/1.25	   f(x) = [0 0 1]x >= [0 0 0]x = ?1(a(),x)
3.25/1.25	          [0 0 0]     [0 0 0]             
3.25/1.25	   
3.25/1.25	            [2 0 0]    [0]    [0]                   
3.25/1.25	   g(x,x) = [0 0 0]x + [0] >= [0] = g(f(a()),f(b()))
3.25/1.25	            [0 0 1]    [1]    [1]                   
3.25/1.25	  problem:
3.25/1.25	   f(x) -> ?1(a(),x)
3.25/1.25	   g(x,x) -> g(f(a()),f(b()))
3.25/1.25	  DP Processor:
3.25/1.25	   DPs:
3.25/1.25	    g#(x,x) -> f#(b())
3.25/1.25	    g#(x,x) -> f#(a())
3.25/1.25	    g#(x,x) -> g#(f(a()),f(b()))
3.25/1.25	   TRS:
3.25/1.25	    f(x) -> ?1(a(),x)
3.25/1.25	    g(x,x) -> g(f(a()),f(b()))
3.25/1.25	   TDG Processor:
3.25/1.25	    DPs:
3.25/1.25	     g#(x,x) -> f#(b())
3.25/1.25	     g#(x,x) -> f#(a())
3.25/1.25	     g#(x,x) -> g#(f(a()),f(b()))
3.25/1.25	    TRS:
3.25/1.25	     f(x) -> ?1(a(),x)
3.25/1.25	     g(x,x) -> g(f(a()),f(b()))
3.25/1.25	    graph:
3.25/1.25	     g#(x,x) -> g#(f(a()),f(b())) -> g#(x,x) -> g#(f(a()),f(b()))
3.25/1.25	     g#(x,x) -> g#(f(a()),f(b())) -> g#(x,x) -> f#(a())
3.25/1.25	     g#(x,x) -> g#(f(a()),f(b())) -> g#(x,x) -> f#(b())
3.25/1.25	    SCC Processor:
3.25/1.25	     #sccs: 1
3.25/1.25	     #rules: 1
3.25/1.25	     #arcs: 3/9
3.25/1.25	     DPs:
3.25/1.25	      g#(x,x) -> g#(f(a()),f(b()))
3.25/1.25	     TRS:
3.25/1.25	      f(x) -> ?1(a(),x)
3.25/1.25	      g(x,x) -> g(f(a()),f(b()))
3.25/1.25	     CDG Processor:
3.25/1.25	      DPs:
3.25/1.25	       g#(x,x) -> g#(f(a()),f(b()))
3.25/1.25	      TRS:
3.25/1.25	       f(x) -> ?1(a(),x)
3.25/1.25	       g(x,x) -> g(f(a()),f(b()))
3.25/1.25	      graph:
3.25/1.25	       
3.25/1.25	      Qed
3.25/1.25	
4.13/1.40	EOF