J, 1717 15 bytes
-2 bytes thanks to Jonah!
#<.(-:'ab'#~2&#-:@#)'ab'#~#
This works correctly for giving falsey for the empty string. Error is falsey.
OldOther versions:
<e.'ab'<@#"{~#\ NB. alternate 15 bytes, thanks to Jonah
#<.(-:'ab'#~-:@#)
NB. the following do not handle the empty string correctly
-:'ab'#~-:@#
2&#-:'ab'#~# NB. thanks to miles
Proof and explanation
Outdated, but applicable to the old 17 byte version.
The main verb is a fork consisting of these three verbs:
# <. (-:'ab'#~-:@#)
This means, "The lesser of (<.
) the length (#
) and the result of the right tine ((-:'ab'#~-:@#)
)".
The right tine is a 4-train, consisting of:
(-:) ('ab') (#~) (-:@#)
Let k
represent our input. Then, this is equivalent to:
k -: ('ab' #~ -:@#) k
-:
is the match operator, so the leading -:
tests for invariance under the monadic fork 'ab' #~ -:@#
.
Since the left tine of the fork is a verb, it becomes a constant function. So, the fork is equivalent to:
'ab' #~ (-:@# k)
The right tine of the fork halves (-:
) the length (#
) of k
. Observe #
:
1 # 'ab'
'ab'
2 # 'ab'
'aabb'
3 # 'ab'
'aaabbb'
'ab' #~ 3
'aaabbb'
Now, this is k
only on valid inputs, so we are done here. #
errors for odd-length strings, which never satisfies the language, so there we are also done.
Combined with the lesser of the length and this, the empty string, which is not a part of our language, yields its length, 0
, and we are done with it all.