structure PDA (Q T S : Type) [Fintype Q] [Fintype T] [Fintype S] : Type

• initial_state : Q
• start_symbol : S
• final_states : Set Q
• transition_fun : Q → T → S → Set (Q × List S)
• transition_fun' : Q → S → Set (Q × List S)
• finite (q : Q) (a : T) (Z : S) : (self.transition_fun q a Z).Finite
• finite' (q : Q) (Z : S) : (self.transition_fun' q Z).Finite

structure PDA.conf {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (p : PDA Q T S) : Type

• state : Q
• input : List T
• stack : List S

theorem PDA.conf.ext_iff {Q T S : Type} {inst✝ : Fintype Q} {inst✝¹ : Fintype T} {inst✝² : Fintype S} {p : PDA Q T S} {x y : p.conf} : x = y ↔ x.state = y.state ∧ x.input = y.input ∧ x.stack = y.stack

theorem PDA.conf.ext {Q T S : Type} {inst✝ : Fintype Q} {inst✝¹ : Fintype T} {inst✝² : Fintype S} {p : PDA Q T S} {x y : p.conf} (state : x.state = y.state) (input : x.input = y.input) (stack : x.stack = y.stack) : x = y

@[reducible, inline]

abbrev PDA.conf.appendInput {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} (r : pda.conf) (x : List T) : pda.conf

Equations

• r.appendInput x = { state := r.state, input := r.input ++ x, stack := r.stack }

@[reducible, inline]

abbrev PDA.conf.appendStack {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} (r : pda.conf) (β : List S) : pda.conf

Equations

• r.appendStack β = { state := r.state, input := r.input, stack := r.stack ++ β }

@[reducible, inline]

abbrev PDA.conf.stackPostfix {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} (r : pda.conf) (β : List S) : Prop

Equations

• r.stackPostfix β = ∃ (α : List S), r.stack = α ++ β

@[reducible, inline]

abbrev PDA.conf.stackPostfixNontriv {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} (r : pda.conf) (β : List S) : Prop

Equations

• r.stackPostfixNontriv β = ∃ (α : List S), α.length > 0 ∧ r.stack = α ++ β

def PDA.step {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} (r₁ : pda.conf) : Set pda.conf

Equations

• One or more equations did not get rendered due to their size.
• PDA.step { state := q, input := [], stack := Z :: α } = {r₂ : pda.conf | ∃ (p : Q) (β : List S), (p, β) ∈ pda.transition_fun' q Z ∧ r₂ = { state := p, input := [], stack := β ++ α }}
• PDA.step { state := state, input := input, stack := [] } = ∅

def PDA.Reaches₁ {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} (r₁ r₂ : pda.conf) : Prop

Equations

• PDA.Reaches₁ r₁ r₂ = (r₂ ∈ PDA.step r₁)

def PDA.Reaches {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} : pda.conf → pda.conf → Prop

Equations

• PDA.Reaches = Relation.ReflTransGen PDA.Reaches₁

inductive PDA.ReachesIn {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} : ℕ → pda.conf → pda.conf → Prop

• refl {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} (r₁ : pda.conf) : ReachesIn 0 r₁ r₁
• step {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {n : ℕ} {r₁ r₂ r₃ : pda.conf} : ReachesIn n r₁ r₂ → Reaches₁ r₂ r₃ → ReachesIn (n + 1) r₁ r₃

def PDA.acceptsByEmptyStack {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (pda : PDA Q T S) : Language T

Equations

• pda.acceptsByEmptyStack = {w : List T | ∃ (q : Q), PDA.Reaches { state := pda.initial_state, input := w, stack := [pda.start_symbol] } { state := q, input := [], stack := [] }}

def PDA.acceptsByFinalState {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (pda : PDA Q T S) : Language T

Equations

• One or more equations did not get rendered due to their size.

theorem PDA.Reaches.refl {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} (r₁ : pda.conf) : Reaches r₁ r₁

theorem PDA.reachesIn.refl {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} (r₁ : pda.conf) : ReachesIn 0 r₁ r₁

theorem PDA.reachesIn_zero {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} (h : ReachesIn 0 r₁ r₂) : r₁ = r₂

theorem PDA.reaches₁_iff_reachesIn_one {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} : Reaches₁ r₁ r₂ ↔ ReachesIn 1 r₁ r₂

theorem PDA.reachesIn_of_n_one {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ r₃ : pda.conf} {n : ℕ} (h₁ : ReachesIn n r₁ r₂) (h₂ : ReachesIn 1 r₂ r₃) : ReachesIn (n + 1) r₁ r₃

theorem PDA.reachesIn_one {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} : ReachesIn 1 r₁ r₂ ↔ r₂ ∈ step r₁

theorem PDA.reachesIn_iff_split_last {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} {n : ℕ} : (∃ (c : pda.conf), ReachesIn n r₁ c ∧ ReachesIn 1 c r₂) ↔ ReachesIn (n + 1) r₁ r₂

theorem PDA.reachesIn_of_one_n {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ r₃ : pda.conf} {n : ℕ} (h₁ : ReachesIn 1 r₁ r₂) (h₂ : ReachesIn n r₂ r₃) : ReachesIn (n + 1) r₁ r₃

theorem PDA.reachesIn_iff_split_first {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} {n : ℕ} : (∃ (c : pda.conf), ReachesIn 1 r₁ c ∧ ReachesIn n c r₂) ↔ ReachesIn (n + 1) r₁ r₂

theorem PDA.ReachesIn.trans {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ r₃ : pda.conf} {n m : ℕ} (h₁ : ReachesIn n r₁ r₂) (h₂ : ReachesIn m r₂ r₃) : ∃ k ≤ n + m, ReachesIn k r₁ r₃

theorem PDA.reaches_iff_reachesIn {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} : Reaches r₁ r₂ ↔ ∃ (n : ℕ), ReachesIn n r₁ r₂

theorem PDA.Reaches.trans {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ r₃ : pda.conf} (h₁ : Reaches r₁ r₂) (h₂ : Reaches r₂ r₃) : Reaches r₁ r₃

theorem PDA.decreasing_input_one' {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} (h : ReachesIn 1 r₁ r₂) : ∃ (w : List T), r₁.input = w ++ r₂.input

theorem PDA.decreasing_input_one {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} (h : ReachesIn 1 r₁ r₂) : ∃ (w : List T), r₁.input = w ++ r₂.input

theorem PDA.decreasing_input {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} (h : Reaches r₁ r₂) : ∃ (w : List T), r₁.input = w ++ r₂.input

theorem PDA.unconsumed_input_one {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} (x : List T) : ReachesIn 1 r₁ r₂ ↔ ReachesIn 1 (r₁.appendInput x) (r₂.appendInput x)

theorem PDA.unconsumed_input_N {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} {n : ℕ} (x : List T) : ReachesIn n r₁ r₂ ↔ ReachesIn n (r₁.appendInput x) (r₂.appendInput x)

theorem PDA.unconsumed_input {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} (x : List T) : Reaches r₁ r₂ ↔ Reaches (r₁.appendInput x) (r₂.appendInput x)

theorem PDA.reachesIn_pos_of_not_self {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} {n : ℕ} (h : r₁ ≠ r₂) : ReachesIn n r₁ r₂ → n > 0

theorem PDA.reachesIn_one_on_empty_stack {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {q p : Q} {w w' : List T} {α : List S} : ¬ReachesIn 1 { state := q, input := w, stack := [] } { state := p, input := w', stack := α }

theorem PDA.reaches_on_empty_stack {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {q p : Q} {w w' : List T} {α : List S} : Reaches { state := q, input := w, stack := [] } { state := p, input := w', stack := α } → w = w' ∧ α = [] ∧ q = p

theorem PDA.reaches_of_reachesIn {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {r₁ r₂ : pda.conf} {n : ℕ} (h : ReachesIn n r₁ r₂) : Reaches r₁ r₂

theorem PDA.reaches₁_push {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {q : Q} {x : List T} {Z : S} {γ : List S} {c : pda.conf} (h : Reaches₁ { state := q, input := x, stack := Z :: γ } c) : (∃ (a : T) (y : List T) (p : Q) (α : List S), x = a :: y ∧ c = { state := p, input := y, stack := α ++ γ } ∧ (p, α) ∈ pda.transition_fun q a Z) ∨ ∃ (p : Q) (α : List S), c = { state := p, input := x, stack := α ++ γ } ∧ (p, α) ∈ pda.transition_fun' q Z

theorem PDA.split_stack {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {n : ℕ} {q p : Q} {x : List T} {α β : List S} (h : ReachesIn n { state := q, input := x, stack := α ++ β } { state := p, input := [], stack := [] }) : ∃ (q₁ : Q) (m₁ : ℕ) (m₂ : ℕ) (y₁ : List T) (y₂ : List T), x = y₁ ++ y₂ ∧ m₁ ≤ n ∧ m₂ ≤ n ∧ ReachesIn m₁ { state := q, input := y₁, stack := α } { state := q₁, input := [], stack := [] } ∧ ReachesIn m₂ { state := q₁, input := y₂, stack := β } { state := p, input := [], stack := [] }

theorem PDA.Reaches₁.append_stack {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {x y : List T} {α β : List S} {q p : Q} (γ : List S) (h : Reaches₁ { state := q, input := x, stack := α } { state := p, input := y, stack := β }) : Reaches { state := q, input := x, stack := α ++ γ } { state := p, input := y, stack := β ++ γ }

theorem PDA.Reaches.append_stack {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {pda : PDA Q T S} {x y : List T} {α β : List S} {q p : Q} (h : Reaches { state := q, input := x, stack := α } { state := p, input := y, stack := β }) (γ : List S) : Reaches { state := q, input := x, stack := α ++ γ } { state := p, input := y, stack := β ++ γ }

theorem PDA.reaches1_of_same_transitions {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (P₁ P₂ : PDA Q T S) (ht : P₁.transition_fun = P₂.transition_fun) (ht' : P₁.transition_fun' = P₂.transition_fun') (q q' : Q) (w w' : List T) (γ γ' : List S) : Reaches₁ { state := q, input := w, stack := γ } { state := q', input := w', stack := γ' } ↔ Reaches₁ { state := q, input := w, stack := γ } { state := q', input := w', stack := γ' }

Two PDAs with the same transition functions have the same single-step relation.

theorem PDA.reaches_of_same_transitions {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (P₁ P₂ : PDA Q T S) (ht : P₁.transition_fun = P₂.transition_fun) (ht' : P₁.transition_fun' = P₂.transition_fun') (c₁ c₂ : P₁.conf) (h : Reaches c₁ c₂) : Reaches { state := c₁.state, input := c₁.input, stack := c₁.stack } { state := c₂.state, input := c₂.input, stack := c₂.stack }

Two PDAs with the same transition functions have the same multi-step relation.

def PDA.is_PDA_emptyStack {T : Type} [Fintype T] (L : Language T) : Prop

Equations

• PDA.is_PDA_emptyStack L = ∃ (Q : Type) (S : Type) (x : Fintype Q) (x_1 : Fintype S) (M : PDA Q T S), M.acceptsByEmptyStack = L

@[reducible, inline]

abbrev PDA.is_PDA {T : Type} [Fintype T] (L : Language T) : Prop

A language over a finite terminal alphabet is accepted by some PDA via empty-stack acceptance.

Equations

• PDA.is_PDA L = PDA.is_PDA_emptyStack L

@[simp]

theorem PDA.is_PDA_emptyStack_iff_is_PDA {T : Type} [Fintype T] {L : Language T} : is_PDA_emptyStack L ↔ is_PDA L

def PDA.is_PDA_finalState {T : Type} [Fintype T] (L : Language T) : Prop

A language over a finite terminal alphabet is accepted by some PDA via final-state acceptance.

Equations

• PDA.is_PDA_finalState L = ∃ (Q : Type) (S : Type) (x : Fintype Q) (x_1 : Fintype S) (M : PDA Q T S), M.acceptsByFinalState = L

def PDA.EmptyStackClass {T : Type} [Fintype T] : Set (Language T)

The class of languages recognized by PDAs via empty-stack acceptance.

Equations

• PDA.EmptyStackClass = setOf PDA.is_PDA

def PDA.Class {T : Type} [Fintype T] : Set (Language T)

The class of PDA-recognizable languages.

This lives under PDA.Class because the top-level name PDA is already used by the automaton structure.

Equations

• @PDA.Class = @PDA.EmptyStackClass

def PDA.FinalStateClass {T : Type} [Fintype T] : Set (Language T)

The class of languages recognized by PDAs via final-state acceptance.

Equations

• PDA.FinalStateClass = setOf PDA.is_PDA_finalState