Lines Matching defs:LEN
155 (* Represent |w| by LEN w. HOL's built-in length function on lists *)
160 `(LEN(N w) = LENGTH w)
162 (LEN(W w) = LENGTH w)
164 (LEN(S w) = LENGTH w)`;
170 val LEN =
172 (``(LEN(N w * a) = LEN(N w) + LEN a)
174 (LEN(W w * a) = LEN(W w))
176 (LEN(S w * a) = LEN(S w))``,
243 (v = W[]) \/ (~(IS_STRONG v) /\ (LEN v = 1) /\ B_SEM (A_ELEM v 0) b))
315 (``LEN(WEAKEN w) = LEN w``,
477 (``!v. IS_WEAK v /\ (LEN v = 0) = (v = W[])``,