4.37/1.99	MAYBE
4.37/1.99	
4.37/1.99	Proof:
4.37/2.00	ConCon could not decide confluence of the system.
4.37/2.00	\cite{ALS94}, Theorem 4.1 does not apply.
4.37/2.00	This system is of type 3 or smaller.
4.37/2.00	This system is strongly deterministic.
4.37/2.00	This system is of type 3 or smaller.
4.37/2.00	This system is deterministic.
4.37/2.00	This system is non-terminating.
4.37/2.00	Call external tool:
4.37/2.00	./ttt2.sh
4.37/2.00	Input:
4.37/2.00	(VAR y' x'' x y'' y x')
4.37/2.00	(RULES
4.37/2.00	  f(x', x'') -> ?1(x', x', x'')
4.37/2.00	  ?1(x, x', x'') -> ?2(x'', x', x'', x)
4.37/2.00	  ?2(x, x', x'', x) -> h(x, f(x, b))
4.37/2.00	  f(g(y'), y'') -> ?3(y', y', y'')
4.37/2.00	  ?3(y, y', y'') -> ?4(y'', y', y'', y)
4.37/2.00	  ?4(y, y', y'', y) -> h(y, f(g(y), a))
4.37/2.00	  a -> b
4.37/2.00	)
4.37/2.00	
4.37/2.00	 Unfolding Processor:
4.37/2.00	  loop length: 3
4.37/2.00	  terms:
4.37/2.00	   f(b(),b())
4.37/2.00	   ?1(b(),b(),b())
4.37/2.00	   ?2(b(),b(),b(),b())
4.37/2.00	  context: h(b(),[])
4.37/2.00	  substitution:
4.37/2.00	   
4.37/2.00	  Qed
4.37/2.00	ConCon could not decide if this system is quasi-decreasing.
4.37/2.00	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
4.37/2.00	This system is of type 3 or smaller.
4.37/2.00	This system is deterministic.
4.37/2.00	This system is non-terminating.
4.37/2.00	Call external tool:
4.37/2.00	./ttt2.sh
4.37/2.00	Input:
4.37/2.00	(VAR y' x'' x y'' y x')
4.37/2.00	(RULES
4.37/2.00	  f(x', x'') -> ?1(x', x', x'')
4.37/2.00	  ?1(x, x', x'') -> ?2(x'', x', x'', x)
4.37/2.00	  ?2(x, x', x'', x) -> h(x, f(x, b))
4.37/2.00	  f(g(y'), y'') -> ?3(y', y', y'')
4.37/2.00	  ?3(y, y', y'') -> ?4(y'', y', y'', y)
4.37/2.00	  ?4(y, y', y'', y) -> h(y, f(g(y), a))
4.37/2.00	  a -> b
4.37/2.00	)
4.37/2.00	
4.37/2.00	 Unfolding Processor:
4.37/2.00	  loop length: 3
4.37/2.00	  terms:
4.37/2.00	   f(b(),b())
4.37/2.00	   ?1(b(),b(),b())
4.37/2.00	   ?2(b(),b(),b(),b())
4.37/2.00	  context: h(b(),[])
4.37/2.00	  substitution:
4.37/2.00	   
4.37/2.00	  Qed
4.37/2.00	
4.37/2.03	EOF