127.06/31.32	MAYBE
127.06/31.32	
127.06/31.32	Proof:
127.06/31.32	ConCon could not decide confluence of the system.
127.06/31.32	\cite{ALS94}, Theorem 4.1 does not apply.
127.06/31.32	This system is of type 3 or smaller.
127.06/31.32	This system is strongly deterministic.
127.06/31.32	This system is of type 3 or smaller.
127.06/31.32	This system is deterministic.
127.06/31.32	ConCon could not decide if this system is quasi-decreasing.
127.06/31.32	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
127.06/31.32	This system is of type 3 or smaller.
127.06/31.32	This system is deterministic.
127.06/31.32	System R transformed to U(R).
127.06/31.32	The external tool could not decide termination of the system.
127.06/31.32	Call external tool:
127.06/31.32	./ttt2.sh
127.06/31.32	Input:
127.06/31.32	(VAR st_2 x t in_2 pid st_3 n h m st_1 in_3)
127.06/31.32	(RULES
127.06/31.32	  fstsplit(0, x) -> nil
127.06/31.32	  fstsplit(s(n), nil) -> nil
127.06/31.32	  fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
127.06/31.32	  sndsplit(0, x) -> x
127.06/31.32	  sndsplit(s(n), nil) -> nil
127.06/31.32	  sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
127.06/31.32	  empty(nil) -> true
127.06/31.32	  empty(cons(h, t)) -> false
127.06/31.32	  leq(0, m) -> true
127.06/31.32	  leq(s(n), 0) -> false
127.06/31.32	  leq(s(n), s(m)) -> leq(n, m)
127.06/31.32	  length(nil) -> 0
127.06/31.32	  length(cons(h, t)) -> s(length(t))
127.06/31.32	  app(nil, x) -> x
127.06/31.32	  app(cons(h, t), x) -> cons(h, app(t, x))
127.06/31.32	  map_f(pid, nil) -> nil
127.06/31.32	  map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
127.06/31.32	  head(cons(h, t)) -> h
127.06/31.32	  tail(cons(h, t)) -> t
127.06/31.32	  ?1(false, st_2, in_2, st_3, m, st_1, in_3) -> ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
127.06/31.32	  ring(st_1, in_2, st_2, in_3, st_3, m) -> ?1(empty(fstsplit(m, st_1)), st_2, in_2, st_3, m, st_1, in_3)
127.06/31.32	  ?11(false, st_2, in_2, st_3, m, st_1, in_3) -> ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
127.06/31.32	  ?10(true, st_2, in_2, st_3, m, st_1, in_3) -> ?11(empty(fstsplit(m, st_2)), st_2, in_2, st_3, m, st_1, in_3)
127.06/31.32	  ring(st_1, in_2, st_2, in_3, st_3, m) -> ?10(leq(m, length(st_2)), st_2, in_2, st_3, m, st_1, in_3)
127.06/31.32	  ?3(false, st_2, in_2, st_3, m, st_1, in_3) -> ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
127.06/31.32	  ?2(false, st_2, in_2, st_3, m, st_1, in_3) -> ?3(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_2, in_2, st_3, m, st_1, in_3)
127.06/31.32	  ring(st_1, in_2, st_2, in_3, st_3, m) -> ?2(leq(m, length(st_2)), st_2, in_2, st_3, m, st_1, in_3)
127.06/31.32	  ?4(true, st_2, in_2, st_3, m, st_1, in_3) -> ring(st_1, tail(in_2), st_2, in_3, st_3, m)
127.06/31.32	  ring(st_1, in_2, st_2, in_3, st_3, m) -> ?4(empty(map_f(two, head(in_2))), st_2, in_2, st_3, m, st_1, in_3)
127.06/31.32	  ?6(false, st_2, in_2, st_3, m, st_1, in_3) -> ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
127.06/31.32	  ?5(true, st_2, in_2, st_3, m, st_1, in_3) -> ?6(empty(fstsplit(m, st_3)), st_2, in_2, st_3, m, st_1, in_3)
127.06/31.32	  ring(st_1, in_2, st_2, in_3, st_3, m) -> ?5(leq(m, length(st_3)), st_2, in_2, st_3, m, st_1, in_3)
127.06/31.32	  ?8(false, st_2, in_2, st_3, m, st_1, in_3) -> ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
127.06/31.32	  ?7(false, st_2, in_2, st_3, m, st_1, in_3) -> ?8(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_2, in_2, st_3, m, st_1, in_3)
127.06/31.32	  ring(st_1, in_2, st_2, in_3, st_3, m) -> ?7(leq(m, length(st_3)), st_2, in_2, st_3, m, st_1, in_3)
127.06/31.32	  ?9(true, st_2, in_2, st_3, m, st_1, in_3) -> ring(st_1, in_2, st_2, tail(in_3), st_3, m)
127.06/31.32	  ring(st_1, in_2, st_2, in_3, st_3, m) -> ?9(empty(map_f(three, head(in_3))), st_2, in_2, st_3, m, st_1, in_3)
127.06/31.32	)
127.06/31.32	
127.06/31.32	
127.06/31.33	EOF