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