YES(?,O(n^1))
728.04/297.09	YES(?,O(n^1))
728.04/297.09	
728.04/297.09	We are left with following problem, upon which TcT provides the
728.04/297.09	certificate YES(?,O(n^1)).
728.04/297.09	
728.04/297.09	Strict Trs:
728.04/297.09	  { t(o(x1)) -> m(a(x1))
728.04/297.09	  , t(e(x1)) -> n(s(x1))
728.04/297.09	  , o(m(a(x1))) -> t(e(n(x1)))
728.04/297.09	  , a(l(x1)) -> a(t(x1))
728.04/297.09	  , n(s(x1)) -> a(l(a(t(x1))))
728.04/297.09	  , s(a(x1)) -> l(a(t(o(m(a(t(e(x1)))))))) }
728.04/297.09	Obligation:
728.04/297.09	  derivational complexity
728.04/297.09	Answer:
728.04/297.09	  YES(?,O(n^1))
728.04/297.09	
728.04/297.09	The problem is match-bounded by 8. The enriched problem is
728.04/297.09	compatible with the following automaton.
728.04/297.09	{ t_0(1) -> 1
728.04/297.09	, t_1(1) -> 6
728.04/297.09	, t_1(4) -> 1
728.04/297.09	, t_1(10) -> 6
728.04/297.09	, t_1(12) -> 11
728.04/297.09	, t_1(16) -> 15
728.04/297.09	, t_2(1) -> 9
728.04/297.09	, t_2(2) -> 7
728.04/297.09	, t_2(10) -> 7
728.04/297.09	, t_2(19) -> 18
728.04/297.09	, t_2(23) -> 22
728.04/297.09	, t_2(29) -> 12
728.04/297.09	, t_3(1) -> 36
728.04/297.09	, t_3(5) -> 38
728.04/297.09	, t_3(6) -> 36
728.04/297.09	, t_3(7) -> 36
728.04/297.09	, t_3(8) -> 33
728.04/297.09	, t_3(31) -> 19
728.04/297.09	, t_3(33) -> 36
728.04/297.09	, t_3(44) -> 43
728.04/297.09	, t_3(48) -> 47
728.04/297.09	, t_3(56) -> 36
728.04/297.09	, t_4(6) -> 41
728.04/297.09	, t_4(7) -> 41
728.04/297.09	, t_4(30) -> 60
728.04/297.09	, t_4(33) -> 41
728.04/297.09	, t_4(35) -> 55
728.04/297.09	, t_4(37) -> 56
728.04/297.09	, t_4(53) -> 44
728.04/297.09	, t_4(56) -> 41
728.04/297.09	, t_4(69) -> 68
728.04/297.09	, t_4(73) -> 72
728.04/297.09	, t_5(7) -> 63
728.04/297.09	, t_5(32) -> 66
728.04/297.09	, t_5(33) -> 63
728.04/297.09	, t_5(40) -> 57
728.04/297.09	, t_5(56) -> 63
728.04/297.09	, t_5(59) -> 79
728.04/297.09	, t_5(77) -> 69
728.04/297.09	, t_6(33) -> 84
728.04/297.09	, t_6(54) -> 87
728.04/297.09	, t_6(56) -> 84
728.04/297.09	, t_6(62) -> 80
728.04/297.09	, t_6(65) -> 81
728.04/297.09	, t_7(78) -> 93
728.04/297.09	, t_7(83) -> 89
728.04/297.09	, t_7(86) -> 90
728.04/297.09	, t_8(92) -> 94
728.04/297.09	, o_0(1) -> 1
728.04/297.09	, o_1(13) -> 12
728.04/297.09	, o_2(20) -> 19
728.04/297.09	, o_3(45) -> 44
728.04/297.09	, o_4(70) -> 69
728.04/297.09	, m_0(1) -> 1
728.04/297.09	, m_1(2) -> 1
728.04/297.09	, m_1(2) -> 6
728.04/297.09	, m_1(2) -> 9
728.04/297.09	, m_1(2) -> 36
728.04/297.09	, m_1(14) -> 13
728.04/297.09	, m_2(21) -> 20
728.04/297.09	, m_2(24) -> 11
728.04/297.09	, m_3(25) -> 18
728.04/297.09	, m_3(46) -> 45
728.04/297.09	, m_4(49) -> 43
728.04/297.09	, m_4(71) -> 70
728.04/297.09	, m_5(74) -> 68
728.04/297.09	, a_0(1) -> 1
728.04/297.09	, a_1(1) -> 2
728.04/297.09	, a_1(6) -> 1
728.04/297.09	, a_1(6) -> 2
728.04/297.09	, a_1(6) -> 5
728.04/297.09	, a_1(11) -> 10
728.04/297.09	, a_1(15) -> 14
728.04/297.09	, a_2(7) -> 1
728.04/297.09	, a_2(7) -> 2
728.04/297.09	, a_2(7) -> 5
728.04/297.09	, a_2(7) -> 6
728.04/297.09	, a_2(7) -> 9
728.04/297.09	, a_2(7) -> 36
728.04/297.09	, a_2(9) -> 8
728.04/297.09	, a_2(13) -> 24
728.04/297.09	, a_2(18) -> 17
728.04/297.09	, a_2(22) -> 21
728.04/297.09	, a_3(20) -> 25
728.04/297.09	, a_3(33) -> 1
728.04/297.09	, a_3(33) -> 2
728.04/297.09	, a_3(33) -> 5
728.04/297.09	, a_3(33) -> 6
728.04/297.09	, a_3(33) -> 9
728.04/297.09	, a_3(33) -> 36
728.04/297.09	, a_3(34) -> 15
728.04/297.09	, a_3(36) -> 35
728.04/297.09	, a_3(38) -> 37
728.04/297.09	, a_3(43) -> 42
728.04/297.09	, a_3(47) -> 46
728.04/297.09	, a_4(39) -> 22
728.04/297.09	, a_4(41) -> 40
728.04/297.09	, a_4(45) -> 49
728.04/297.09	, a_4(55) -> 15
728.04/297.09	, a_4(56) -> 1
728.04/297.09	, a_4(56) -> 2
728.04/297.09	, a_4(56) -> 5
728.04/297.09	, a_4(56) -> 6
728.04/297.09	, a_4(56) -> 9
728.04/297.09	, a_4(56) -> 36
728.04/297.09	, a_4(58) -> 12
728.04/297.09	, a_4(60) -> 59
728.04/297.09	, a_4(68) -> 67
728.04/297.09	, a_4(72) -> 71
728.04/297.09	, a_5(57) -> 22
728.04/297.09	, a_5(61) -> 47
728.04/297.09	, a_5(63) -> 62
728.04/297.09	, a_5(64) -> 19
728.04/297.09	, a_5(66) -> 65
728.04/297.09	, a_5(70) -> 74
728.04/297.09	, a_5(79) -> 12
728.04/297.09	, a_6(80) -> 47
728.04/297.09	, a_6(81) -> 19
728.04/297.09	, a_6(82) -> 72
728.04/297.09	, a_6(84) -> 83
728.04/297.09	, a_6(85) -> 44
728.04/297.09	, a_6(87) -> 86
728.04/297.09	, a_7(89) -> 72
728.04/297.09	, a_7(90) -> 44
728.04/297.09	, a_7(91) -> 69
728.04/297.09	, a_7(93) -> 92
728.04/297.09	, a_8(94) -> 69
728.04/297.09	, e_0(1) -> 1
728.04/297.09	, e_1(1) -> 16
728.04/297.09	, e_1(5) -> 4
728.04/297.09	, e_1(6) -> 16
728.04/297.09	, e_1(7) -> 16
728.04/297.09	, e_1(33) -> 16
728.04/297.09	, e_1(56) -> 16
728.04/297.09	, e_2(6) -> 23
728.04/297.09	, e_2(7) -> 23
728.04/297.09	, e_2(30) -> 29
728.04/297.09	, e_2(33) -> 23
728.04/297.09	, e_2(56) -> 23
728.04/297.09	, e_3(7) -> 48
728.04/297.09	, e_3(32) -> 31
728.04/297.09	, e_3(33) -> 48
728.04/297.09	, e_3(56) -> 48
728.04/297.09	, e_4(33) -> 73
728.04/297.09	, e_4(54) -> 53
728.04/297.09	, e_4(56) -> 73
728.04/297.09	, e_5(78) -> 77
728.04/297.09	, n_0(1) -> 1
728.04/297.09	, n_1(1) -> 5
728.04/297.09	, n_1(3) -> 1
728.04/297.09	, n_1(3) -> 6
728.04/297.09	, n_1(3) -> 9
728.04/297.09	, n_1(3) -> 36
728.04/297.09	, n_1(6) -> 5
728.04/297.09	, n_1(7) -> 5
728.04/297.09	, n_1(33) -> 5
728.04/297.09	, n_1(56) -> 5
728.04/297.09	, n_2(15) -> 30
728.04/297.09	, n_2(26) -> 15
728.04/297.09	, n_2(27) -> 1
728.04/297.09	, n_3(22) -> 32
728.04/297.09	, n_3(28) -> 22
728.04/297.09	, n_3(50) -> 12
728.04/297.09	, n_4(47) -> 54
728.04/297.09	, n_4(51) -> 47
728.04/297.09	, n_4(52) -> 19
728.04/297.09	, n_5(72) -> 78
728.04/297.09	, n_5(75) -> 72
728.04/297.09	, n_5(76) -> 44
728.04/297.09	, n_6(88) -> 69
728.04/297.09	, s_0(1) -> 1
728.04/297.09	, s_1(1) -> 3
728.04/297.09	, s_2(1) -> 26
728.04/297.09	, s_2(5) -> 27
728.04/297.09	, s_2(6) -> 26
728.04/297.09	, s_2(7) -> 26
728.04/297.09	, s_2(33) -> 26
728.04/297.09	, s_2(56) -> 26
728.04/297.09	, s_3(6) -> 28
728.04/297.09	, s_3(7) -> 28
728.04/297.09	, s_3(30) -> 50
728.04/297.09	, s_3(33) -> 28
728.04/297.09	, s_3(56) -> 28
728.04/297.09	, s_4(7) -> 51
728.04/297.09	, s_4(32) -> 52
728.04/297.09	, s_4(33) -> 51
728.04/297.09	, s_4(56) -> 51
728.04/297.09	, s_5(33) -> 75
728.04/297.09	, s_5(54) -> 76
728.04/297.09	, s_5(56) -> 75
728.04/297.09	, s_6(78) -> 88
728.04/297.09	, l_0(1) -> 1
728.04/297.09	, l_1(2) -> 6
728.04/297.09	, l_1(10) -> 1
728.04/297.09	, l_1(10) -> 3
728.04/297.09	, l_1(10) -> 26
728.04/297.09	, l_2(8) -> 7
728.04/297.09	, l_2(17) -> 3
728.04/297.09	, l_2(17) -> 26
728.04/297.09	, l_2(17) -> 27
728.04/297.09	, l_3(35) -> 34
728.04/297.09	, l_3(37) -> 33
728.04/297.09	, l_3(42) -> 26
728.04/297.09	, l_3(42) -> 27
728.04/297.09	, l_3(42) -> 28
728.04/297.09	, l_4(40) -> 39
728.04/297.09	, l_4(59) -> 58
728.04/297.09	, l_4(67) -> 28
728.04/297.09	, l_5(62) -> 61
728.04/297.09	, l_5(65) -> 64
728.04/297.09	, l_6(83) -> 82
728.04/297.09	, l_6(86) -> 85
728.04/297.09	, l_7(92) -> 91 }
728.04/297.09	
728.04/297.09	Hurray, we answered YES(?,O(n^1))
728.20/297.10	EOF