# A bottom-first PDA run accepting aabb

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

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-pushdown-automaton-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

The specified PDA has a finite run consuming aabb and ending at final f with stack [Z].

The full transition relation and bottom-first/top-last stack; final-state rather than empty-stack acceptance.





## Givens and symbols


- calc


- G1 — Q={q,p,f}, input={a,b}, stack={Z,A}, all disjoint; start q,bottom Z,finals {f}. Transitions [from,input or null,top,to,replacement bottom-to-top] are [q,a,Z,q,[Z,A]],[q,a,A,q,[A,A]],[q,b,A,p,[]],[p,b,A,p,[]],[p,null,Z,f,[Z]],[q,null,Z,f,[Z]]. Word aabb.


- Z — bottom protected from underflow
- null — input-free epsilon
- i — consumed input length





## Rules and sources


- calc · prerequisite — Assume finite sets, finite strings and indices, stepwise function updates and induction on natural numbers; epsilon denotes the length-zero word.
- mko_definition · cited — The PDA tuple specifies finite states Q, input/stack alphabets, start q0, bottom Z, final states and a transition relation. Each transition is [from state,input symbol or null,required top,to state,replacement bottom-to-top]. null denotes epsilon and consumes no input. A stack is bottom-first/top-last and its bottom may not underflow. An acceptance witness is a finite run consuming all input and ending in a final state. Do not substitute empty-stack acceptance. Bounded-search failure does not prove rejection; neither CFG equivalence nor determinism follows automatically. · mko-pushdown-automaton





## Main derivation

S01 · impliesBefore

Q=\{q,p,f\},\quad\Sigma=\{a,b\},\quad\Gamma=\{Z,A\}

After

\begin{array}{c|c|c|c|c}q&a&Z&q&[Z,A]\\q&a&A&q&[A,A]\\q&b&A&p&[]\\p&b&A&p&[]\\p&\text{null}&Z&f&[Z]\\q&\text{null}&Z&f&[Z]\end{array}

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

All six relation entries are valid; bottom Z is replaced only by bottom-preserving [Z,A] or [Z], preventing underflow.



S02 · impliesBefore

w=aabb,\quad |w|=4

After

[q,0,[Z]]

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Initialize at position zero with stack consisting only of bottom Z.



S03 · impliesBefore

[q,0,[Z]]

After

[q,1,[Z,A]]

Conditions: none

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

Read the first a using [q,a,Z,q,[Z,A]], retaining the bottom and pushing A.



S04 · impliesBefore

[q,1,[Z,A]]

After

[q,2,[Z,A,A]]

Conditions: none

Rule: calc · Uses: G1, S01, S03

Leaf basis: calc

Read the second a, replacing the top A by [A,A] while retaining Z below.



S05 · impliesBefore

[q,2,[Z,A,A]]

After

[p,3,[Z,A]]

Conditions: none

Rule: calc · Uses: G1, S01, S04

Leaf basis: calc

Read the first b using [q,b,A,p,[]], popping the rightmost A and entering p.



S06 · impliesBefore

[p,3,[Z,A]]

After

[p,4,[Z]]

Conditions: none

Rule: calc · Uses: G1, S01, S05

Leaf basis: calc

Read the last b using [p,b,A,p,[]], removing the final A and reaching position 4.



S07 · impliesBefore

[p,4,[Z]]

After

[f,4,[Z]]

Conditions: none

Rule: calc · Uses: G1, S01, S06

Leaf basis: calc

Use [p,null,Z,f,[Z]] as an epsilon move, keeping position 4 and preserving bottom.



S08 · impliesBefore

[f,4,[Z]],\quad f\in F,\quad4=|w|

After

aabb\text{ accepted by this finite run}

Conditions: none

Rule: mko_definition · Uses: G1, S02, S03, S04, S05, S06, S07

Leaf basis: mko_definition

All input is consumed and the endpoint is final, meeting the stated convention despite a nonempty stack.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S02, S03, S04, S05, S06, S07 — Taking q's epsilon to f initially leaves position 0 rather than 4 and does not accept aabb.
- S07 · premise_audit · G1, S01, S06 — null consumes no input and cannot replace Z by [].
- S06 · premise_audit · G1, S01, S05 — Input is consumed but p is not final, so a legal epsilon move remains necessary.
- S05 · premise_audit · G1, S01, S04 — Only one top is popped, not the whole stack.
- S04 · premise_audit · G1, S01, S03 — The right end is top; the net increase is one A, not two.
- S03 · premise_audit · G1, S01, S02 — The replacement includes Z; using [A] would lose the bottom.
- S02 · premise_audit · G1, S01 — A configuration is [state,position,stack], not [state,next character,stack].
- S01 · premise_audit · G1 — The relation need not be total; replacements are bottom-to-top, and [] pops only an A.





## Error controls and negative controls

Stack directionThe stack is bottom-first/top-last, with pop and replacement at the right end.

Two acceptance gatesRequire both full input and a final state, not empty-stack acceptance.


- The terminal stack must be empty to accept. → reject — The convention is full input plus final f; terminal [Z] is accepted.
- null changes position 4 to 5. → reject — Epsilon consumes no input.
- The initial epsilon to f accepts aabb. → reject — All four symbols remain unread; position 0 is not length 4.





## Result and limitations

The specified PDA has a finite run consuming aabb and ending at final f with stack [Z].







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 4b91e5f3268836475349aa0a7814487dd2f540fb36c66fb88a2f29701b97f326
- original source SHA-256: 4b91e5f3268836475349aa0a7814487dd2f540fb36c66fb88a2f29701b97f326
- 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-pushdown-automaton-01.json)