Metamath Proof Explorer


Theorem lencl

Description: The length of a word is a nonnegative integer. This corresponds to the definition in Section 9.1 of AhoHopUll p. 318. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion lencl W Word S W 0

Proof

Step Hyp Ref Expression
1 wrdfin W Word S W Fin
2 hashcl W Fin W 0
3 1 2 syl W Word S W 0