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