# Star closure with epsilon and a complete length slice

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-regular-expression/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-regular-expression-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Give typed AST semantics, complete bounded enumeration and membership obligations.

Sigma={a,b}; the length≤3 list is explicitly only a slice.





## Givens and symbols


- work


- G1 — Sigma={a,b}. R=concat(star(union(epsilon,symbol(a))),symbol(b)); empty-language is denoted emptyset and the epsilon language is{epsilon}.


- K — sublanguage under star
- S_j — bounded closure iterate





## Rules and sources


- mko_definition · cited — The typed AST permits only empty-language, epsilon, alphabet symbols, union, ordered concatenation and star; every symbol belongs to the explicit alphabet. Its language is defined recursively. Bounded star enumeration uses fixed-point closure with extensional deduplication to terminate epsilon cycles. Word membership must be decided with a sufficient complete length slice, not by absence from an insufficient bound. Unions are canonicalized under permutation and idempotence, while concatenation order is retained. The empty language differs from the language containing the empty word, a shell wildcard is not this core regex AST, and equality through length N does not imply equality of the full languages. · mko-regular-expression
- work · prerequisite — Core regex semantics: empty has no words, epsilon contains the empty word, union is set union, concatenation is ordered word product, and star takes all finite concatenations; bounded closure deduplicates sets.





## Main derivation

S01 · impliesBefore

R=\operatorname{concat}(\operatorname{star}(\operatorname{union}(\varepsilon,a)),b)

After

\text{union binary, concat binary, star unary; }a,b\in\Sigma

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

Validate all AST node types, arities and alphabet symbols.



S02 · impliesBefore

L(\varepsilon)=\{\varepsilon\},\quad L(a)=\{a\}

After

K=L(\operatorname{union}(\varepsilon,a))=\{\varepsilon,a\}

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

Union combines language elements extensionally with deduplication.



S03 · impliesBefore

S_0=\{\varepsilon\},\quad S_{j+1}=S_j\cup\{uv:u\in S_j,v\in K,|uv|\le3\}

After

S_1=\{\varepsilon,a\}

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

Bounded star uses set fixed-point closure; multiplying by epsilon adds nothing new.



S04 · impliesBefore

S_1=\{\varepsilon,a\}

After

S_2=\{\varepsilon,a,aa\},\quad S_3=\{\varepsilon,a,aa,aaa\},\quad S_4=S_3

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

The fourth round stabilizes, listing every a-string of length≤3.



S05 · impliesBefore

L(R)=K^*\{b\}

After

L(R)\cap\Sigma^{\le3}=\{b,ab,aab\}

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

Ordered concatenation appends b on the right, retaining total length≤3.



S06 · impliesBefore

K^*=\{a^m:m\in\mathbb N_0\}

After

L(R)=\{a^mb:m\in\mathbb N_0\}

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

Every K factor is epsilon or a, so concatenation counts a's only; conversely use m a-factors.



S07 · impliesBefore

w=aaab,\quad |w|=4

After

w=a^3b\in L(R),\quad w\notin\{b,ab,aab\}

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

Full semantics decides membership true; absence from the length3 list cannot imply false.



S08 · impliesBefore

\operatorname{concat}(b,\operatorname{star}(a))

After

b\{a^m:m\ge0\}\ne\{a^mb:m\ge0\}\quad(ab\text{ witnesses})

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

Concatenation is not commutative: ab lies in R but not in ba*.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — Union admits permutation and idempotence canonicalization, but concatenation preserves order.
- S07 · premise_audit · G1, S06, work — A bounded membership procedure needs at least a complete length4 slice.
- S06 · premise_audit · G1, S05, work — This is a two-way all-m semantic proof, not inference from the bounded list.
- S05 · premise_audit · G1, S04, work — aaab has length4 and lies outside this slice but may belong to the full language.
- S04 · premise_audit · G1, S03, work — No other symbol belongs to K, so no b or mixed string is generated.
- S03 · premise_audit · G1, S02, work — Deduplication prevents infinite repetition from epsilon cycles.
- S02 · premise_audit · G1, S01, work — The empty language differs from{epsilon}; it contains no element.
- S01 · premise_audit · G1, work — Star applies to a sublanguage, not a shell arbitrary-string wildcard.





## Error controls and negative controls

Epsilon deduplicationUse sets so epsilon products add no duplicate copies.

Slice labelLabel every bounded result with its length limit, without inferring full equivalence.


- The empty language equals{epsilon}. → reject — The latter contains one empty word; the former contains none.
- aaab is a nonmember because absent from the length3 list. → reject — aaab=a³b satisfies full semantics and has length4 outside the slice.
- Concatenation may swap operands. → reject — ab belongs to a*b but not ba*.





## Result and limitations

The full language is{a^m b:m≥0}; its length≤3 slice is{b,ab,aab}, while aaab is still a member.







## Verification and source binding

2 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 477a3a7c717c0ddf0f6208cbbf27ebde9d4743b8722ed272a842db0e6b108780
- original source SHA-256: 477a3a7c717c0ddf0f6208cbbf27ebde9d4743b8722ed272a842db0e6b108780
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-regular-expression-01.json)