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