LanglibTotalization Construction #
This file defines the analyzed DPDA totalizer A from a RegularEpsilonAnalysis A
of M and proves it is an equivalent deciding presentation of the original
final-state DPDA.
The totalizer has finite control TotalState Q (init, sim q b, drain), where
the boolean b records whether M would accept if the input ended at the current
stack, recomputed from the stored stack summaries (AnnotatedStack). On each input
symbol it follows M's input transition where one exists; at a stack top whose
forced epsilon phase diverges (stopsFromSummary false) or where M has no move it
goes to the rejecting drain state and consumes the rest of the input. Its epsilon
transitions replay only stopping epsilon phases of M.
The two correctness results are totalizer_decides (totalizer_total for totality
and totalizer_final_consistent for acceptance consistency) and
totalizer_acceptsByFinalState_eq_original (same language).
Finite control states of the totalized DPDA. The boolean in sim records
whether the original machine would accept if the input ended at the current stack.
- init {Q : Type} : TotalState Q
- sim {Q : Type} : Q → Bool → TotalState Q
- drain {Q : Type} : TotalState Q
Instances For
Equations
- DPDA.instDecidableEqTotalState.decEq DPDA.TotalState.init DPDA.TotalState.init = isTrue ⋯
- DPDA.instDecidableEqTotalState.decEq DPDA.TotalState.init (DPDA.TotalState.sim a a_1) = isFalse ⋯
- DPDA.instDecidableEqTotalState.decEq DPDA.TotalState.init DPDA.TotalState.drain = isFalse ⋯
- DPDA.instDecidableEqTotalState.decEq (DPDA.TotalState.sim a a_1) DPDA.TotalState.init = isFalse ⋯
- DPDA.instDecidableEqTotalState.decEq (DPDA.TotalState.sim a a_1) (DPDA.TotalState.sim b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
- DPDA.instDecidableEqTotalState.decEq (DPDA.TotalState.sim a a_1) DPDA.TotalState.drain = isFalse ⋯
- DPDA.instDecidableEqTotalState.decEq DPDA.TotalState.drain DPDA.TotalState.init = isFalse ⋯
- DPDA.instDecidableEqTotalState.decEq DPDA.TotalState.drain (DPDA.TotalState.sim a a_1) = isFalse ⋯
- DPDA.instDecidableEqTotalState.decEq DPDA.TotalState.drain DPDA.TotalState.drain = isTrue ⋯
Instances For
Equations
- DPDA.instFintypeTotalState = Fintype.ofEquiv (Unit ⊕ (_ : Q✝) × Bool ⊕ Unit) (DPDA.TotalState.proxyTypeEquiv Q✝)
def
DPDA.annotatedReplacement
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(below : AnalysisSummary A)
(β : List S)
:
List (TotalStackSymbol A)
Replacement block for an original stack update above a known suffix summary.
Equations
- DPDA.annotatedReplacement A below β = DPDA.annotateAbove A below β
Instances For
def
DPDA.initialReplacement
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
List (TotalStackSymbol A)
Initial stack expansion: install the original start symbol above the permanent bottom.
Equations
Instances For
theorem
DPDA.erase_annotatedReplacement
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(below : AnalysisSummary A)
(β : List S)
:
theorem
DPDA.erase_annotatedReplacement_append
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(below : AnalysisSummary A)
(β : List S)
(rest : List (TotalStackSymbol A))
:
theorem
DPDA.erase_initialReplacement
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
theorem
DPDA.stackWellAnnotated_initialReplacement
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
theorem
DPDA.stackHasBottom_initialReplacement
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
theorem
DPDA.stackWellAnnotated_annotatedReplacement_append
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{below : AnalysisSummary A}
{rest : List (TotalStackSymbol A)}
(β : List S)
(hbelow : SummaryRepresents A below (eraseAnnotatedStack A rest))
(hrest : StackWellAnnotated A rest)
:
StackWellAnnotated A (annotatedReplacement A below β ++ rest)
theorem
DPDA.stackHasBottom_annotatedReplacement_append
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{below : AnalysisSummary A}
{rest : List (TotalStackSymbol A)}
(β : List S)
(hrest : StackHasBottom A rest)
:
StackHasBottom A (annotatedReplacement A below β ++ rest)
theorem
DPDA.summaryRepresents_replacement
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{below : AnalysisSummary A}
{rest : List (TotalStackSymbol A)}
(β : List S)
(hbelow : SummaryRepresents A below (eraseAnnotatedStack A rest))
:
SummaryRepresents A (AnalysisSummary.above A below β) (eraseAnnotatedStack A (annotatedReplacement A below β ++ rest))
theorem
DPDA.replacement_preserves_annotations
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{Z : S}
{below : AnalysisSummary A}
{rest : List (TotalStackSymbol A)}
(β : List S)
(hstack : StackWellAnnotated A (some (Z, below) :: rest))
:
StackWellAnnotated A (annotatedReplacement A below β ++ rest) ∧ SummaryRepresents A (AnalysisSummary.above A below β) (eraseAnnotatedStack A (annotatedReplacement A below β ++ rest))
theorem
DPDA.replacement_preserves_bottom
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{Z : S}
{below : AnalysisSummary A}
{rest : List (TotalStackSymbol A)}
(β : List S)
(hbottom : StackHasBottom A (some (Z, below) :: rest))
:
StackHasBottom A (annotatedReplacement A below β ++ rest)
theorem
DPDA.initialSummaryRepresents
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
def
DPDA.initialSummary
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
Equations
Instances For
def
DPDA.initialAcceptBit
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
Equations
Instances For
theorem
DPDA.initial_configuration_annotations
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
StackWellAnnotated A (initialReplacement A) ∧ StackHasBottom A (initialReplacement A) ∧ SummaryRepresents A (initialSummary A) (eraseAnnotatedStack A (initialReplacement A))
def
DPDA.simState
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(q : Q)
(summary : AnalysisSummary A)
:
The finite-control state corresponding to an original state and a resulting stack summary.
Equations
- DPDA.simState A q summary = DPDA.TotalState.sim q (DPDA.acceptBit A q summary)
Instances For
def
DPDA.totalizer
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
DPDA (TotalState Q) T (TotalStackSymbol A)
The analyzed totalizer. It follows terminating epsilon phases of M, treats
divergent epsilon phases as stable decision points, and drains any remaining input
to a rejecting state when the original computation cannot consume the next symbol.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
DPDA.simState_mem_final_iff
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(q : Q)
(summary : AnalysisSummary A)
:
theorem
DPDA.sim_mem_final_iff
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(q : Q)
(b : Bool)
:
theorem
DPDA.simState_mem_final_iff_semantic
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q : Q}
{summary : AnalysisSummary A}
{γ : List S}
(hsummary : SummaryRepresents A summary γ)
:
theorem
DPDA.init_mem_final_iff
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
theorem
DPDA.drain_not_mem_final
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
theorem
DPDA.totalizer_empty_step_preserves_final
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{st₁ st₂ : TotalState Q}
{stack₁ stack₂ : List (TotalStackSymbol A)}
(hstep : PDA.Reaches₁ { state := st₁, input := [], stack := stack₁ } { state := st₂, input := [], stack := stack₂ })
:
theorem
DPDA.totalizer_empty_reaches_preserves_final_aux
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{st₁ : TotalState Q}
{stack₁ : List (TotalStackSymbol A)}
{c₂ : (totalizer A).toPDA.conf}
(hreach : PDA.Reaches { state := st₁, input := [], stack := stack₁ } c₂)
:
theorem
DPDA.totalizer_empty_reaches_preserves_final
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{st₁ st₂ : TotalState Q}
{stack₁ stack₂ : List (TotalStackSymbol A)}
(hreach : PDA.Reaches { state := st₁, input := [], stack := stack₁ } { state := st₂, input := [], stack := stack₂ })
:
theorem
DPDA.totalizer_step_deterministic
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{c c₁ c₂ : (totalizer A).toPDA.conf}
(h₁ : PDA.Reaches₁ c c₁)
(h₂ : PDA.Reaches₁ c c₂)
:
theorem
DPDA.totalizer_reachesIn_deterministic
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{n : ℕ}
{c c₁ c₂ : (totalizer A).toPDA.conf}
(h₁ : PDA.ReachesIn n c c₁)
(h₂ : PDA.ReachesIn n c c₂)
:
theorem
DPDA.totalizer_reachesIn_prefix_of_le
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{n m : ℕ}
{c c₁ c₂ : (totalizer A).toPDA.conf}
(hle : n ≤ m)
(h₁ : PDA.ReachesIn n c c₁)
(h₂ : PDA.ReachesIn m c c₂)
:
PDA.Reaches c₁ c₂
theorem
DPDA.totalizer_sim_step_to_original
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q p : Q}
{b b' : Bool}
{input input' : List T}
{stack stack' : List (TotalStackSymbol A)}
(hstep :
PDA.Reaches₁ { state := TotalState.sim q b, input := input, stack := stack }
{ state := TotalState.sim p b', input := input', stack := stack' })
:
PDA.Reaches₁ { state := q, input := input, stack := eraseAnnotatedStack A stack }
{ state := p, input := input', stack := eraseAnnotatedStack A stack' }
theorem
DPDA.totalizer_no_step_to_init
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{c : (totalizer A).toPDA.conf}
{input : List T}
{stack : List (TotalStackSymbol A)}
(hstep : PDA.Reaches₁ c { state := TotalState.init, input := input, stack := stack })
:
theorem
DPDA.totalizer_reaches_original_rep
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(w : List T)
{c : (totalizer A).toPDA.conf}
(hreach : PDA.Reaches { state := TotalState.init, input := w, stack := [none] } c)
:
(c.state = TotalState.init → c.input = w ∧ c.stack = [none]) ∧ ∀ (q : Q) (b : Bool),
c.state = TotalState.sim q b →
PDA.Reaches { state := M.initial_state, input := w, stack := [M.start_symbol] }
{ state := q, input := c.input, stack := eraseAnnotatedStack A c.stack }
theorem
DPDA.totalizer_reaches_sim_to_original
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(w : List T)
{q : Q}
{b : Bool}
{input : List T}
{stack : List (TotalStackSymbol A)}
(hreach :
PDA.Reaches { state := TotalState.init, input := w, stack := [none] }
{ state := TotalState.sim q b, input := input, stack := stack })
:
PDA.Reaches { state := M.initial_state, input := w, stack := [M.start_symbol] }
{ state := q, input := input, stack := eraseAnnotatedStack A stack }
theorem
DPDA.totalizer_reaches_stack_invariants
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(w : List T)
{c : (totalizer A).toPDA.conf}
(hreach : PDA.Reaches { state := TotalState.init, input := w, stack := [none] } c)
:
theorem
DPDA.totalizer_empty_final_to_original_accept
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(w : List T)
{c : (totalizer A).toPDA.conf}
(hreach : PDA.Reaches { state := TotalState.init, input := w, stack := [none] } c)
(hinput : c.input = [])
(hfinal : c.state ∈ (totalizer A).final_states)
:
theorem
DPDA.totalizer_acceptsByFinalState_subset_original
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
theorem
DPDA.totalizer_initial_step
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(w : List T)
:
PDA.Reaches₁ { state := TotalState.init, input := w, stack := [none] }
{ state := simState A M.initial_state (AnalysisSummary.above A (AnalysisSummary.id A) [M.start_symbol]), input := w,
stack := initialReplacement A }
theorem
DPDA.totalizer_initial_reaches
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(w : List T)
:
PDA.Reaches { state := TotalState.init, input := w, stack := [none] }
{ state := simState A M.initial_state (AnalysisSummary.above A (AnalysisSummary.id A) [M.start_symbol]), input := w,
stack := initialReplacement A }
theorem
DPDA.totalizer_accepts_nil_of_original_accept
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(h : [] ∈ M.acceptsByFinalState)
:
theorem
DPDA.totalizer_input_step_of_transition
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q p : Q}
{b : Bool}
{a : T}
{Z : S}
{below : AnalysisSummary A}
{β : List S}
{rest : List (TotalStackSymbol A)}
{w : List T}
(hε : M.epsilon_transition q Z = none)
(hδ : M.transition q a Z = some (p, β))
:
PDA.Reaches₁ { state := TotalState.sim q b, input := a :: w, stack := some (Z, below) :: rest }
{ state := simState A p (AnalysisSummary.above A below β), input := w,
stack := annotatedReplacement A below β ++ rest }
theorem
DPDA.totalizer_input_step_preserves_annotations
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q p : Q}
{b : Bool}
{a : T}
{Z : S}
{below : AnalysisSummary A}
{β : List S}
{rest : List (TotalStackSymbol A)}
{w : List T}
(hε : M.epsilon_transition q Z = none)
(hδ : M.transition q a Z = some (p, β))
(hstack : StackWellAnnotated A (some (Z, below) :: rest))
(hbottom : StackHasBottom A (some (Z, below) :: rest))
:
∃ (stack' : List (TotalStackSymbol A)) (summary' : AnalysisSummary A),
PDA.Reaches₁ { state := TotalState.sim q b, input := a :: w, stack := some (Z, below) :: rest }
{ state := simState A p summary', input := w, stack := stack' } ∧ StackWellAnnotated A stack' ∧ StackHasBottom A stack' ∧ SummaryRepresents A summary' (eraseAnnotatedStack A stack') ∧ eraseAnnotatedStack A stack' = β ++ eraseAnnotatedStack A rest
theorem
DPDA.totalizer_epsilon_step_of_transition
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q p : Q}
{b : Bool}
{Z : S}
{below : AnalysisSummary A}
{β : List S}
{rest : List (TotalStackSymbol A)}
{w : List T}
(hε : M.epsilon_transition q Z = some (p, β))
(hstop : stopsFromSummary A q (fullSummaryOfTop A (some (Z, below))))
:
PDA.Reaches₁ { state := TotalState.sim q b, input := w, stack := some (Z, below) :: rest }
{ state := TotalState.sim p b, input := w, stack := annotatedReplacement A below β ++ rest }
theorem
DPDA.totalizer_epsilon_step_of_epsilonStep
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q p : Q}
{b : Bool}
{γ' : List S}
{top : TotalStackSymbol A}
{rest : List (TotalStackSymbol A)}
{w : List T}
(hstack : StackWellAnnotated A (top :: rest))
(hbottom : StackHasBottom A (top :: rest))
(hstep : M.EpsilonStep (q, eraseAnnotatedStack A (top :: rest)) (p, γ'))
(hstop : ∃ (c' : EpsilonConf Q S), M.EpsilonStopsAt (q, eraseAnnotatedStack A (top :: rest)) c')
:
∃ (stack' : List (TotalStackSymbol A)) (summary' : AnalysisSummary A),
PDA.Reaches₁ { state := TotalState.sim q b, input := w, stack := top :: rest }
{ state := TotalState.sim p b, input := w, stack := stack' } ∧ StackWellAnnotated A stack' ∧ StackHasBottom A stack' ∧ SummaryRepresents A summary' γ' ∧ eraseAnnotatedStack A stack' = γ'
theorem
DPDA.totalizer_epsilonReaches_of_epsilonReaches
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q : Q}
{b : Bool}
{c' : EpsilonConf Q S}
{top : TotalStackSymbol A}
{rest : List (TotalStackSymbol A)}
{w : List T}
(hstack : StackWellAnnotated A (top :: rest))
(hbottom : StackHasBottom A (top :: rest))
(hreach : M.EpsilonReaches (q, eraseAnnotatedStack A (top :: rest)) c')
(hstop : ∃ (cfinal : EpsilonConf Q S), M.EpsilonStopsAt (q, eraseAnnotatedStack A (top :: rest)) cfinal)
:
∃ (stack' : List (TotalStackSymbol A)) (summary' : AnalysisSummary A),
PDA.Reaches { state := TotalState.sim q b, input := w, stack := top :: rest }
{ state := TotalState.sim c'.1 b, input := w, stack := stack' } ∧ StackWellAnnotated A stack' ∧ StackHasBottom A stack' ∧ SummaryRepresents A summary' c'.2 ∧ eraseAnnotatedStack A stack' = c'.2
theorem
DPDA.totalizer_epsilonStopsAt_of_epsilonStopsAt
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q : Q}
{b : Bool}
{cstable : EpsilonConf Q S}
{top : TotalStackSymbol A}
{rest : List (TotalStackSymbol A)}
{w : List T}
(hstack : StackWellAnnotated A (top :: rest))
(hbottom : StackHasBottom A (top :: rest))
(hstops : M.EpsilonStopsAt (q, eraseAnnotatedStack A (top :: rest)) cstable)
:
∃ (stack' : List (TotalStackSymbol A)) (summary' : AnalysisSummary A),
PDA.Reaches { state := TotalState.sim q b, input := w, stack := top :: rest }
{ state := TotalState.sim cstable.1 b, input := w, stack := stack' } ∧ StackWellAnnotated A stack' ∧ StackHasBottom A stack' ∧ SummaryRepresents A summary' cstable.2 ∧ eraseAnnotatedStack A stack' = cstable.2 ∧ M.EpsilonStable cstable
theorem
DPDA.totalizer_input_step_to_drain_of_no_transition
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q : Q}
{b : Bool}
{a : T}
{Z : S}
{below : AnalysisSummary A}
{rest : List (TotalStackSymbol A)}
{w : List T}
(hε : M.epsilon_transition q Z = none)
(hδ : M.transition q a Z = none)
:
theorem
DPDA.totalizer_input_step_to_drain_of_unstopping_epsilon
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q p : Q}
{b : Bool}
{a : T}
{Z : S}
{below : AnalysisSummary A}
{β : List S}
{rest : List (TotalStackSymbol A)}
{w : List T}
(hε : M.epsilon_transition q Z = some (p, β))
(hstop : ¬stopsFromSummary A q (fullSummaryOfTop A (some (Z, below))))
:
theorem
DPDA.totalizer_input_step_to_drain_of_empty_stack
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q : Q}
{b : Bool}
{a : T}
{rest : List (TotalStackSymbol A)}
{w : List T}
:
PDA.Reaches₁ { state := TotalState.sim q b, input := a :: w, stack := none :: rest }
{ state := TotalState.drain, input := w, stack := none :: rest }
theorem
DPDA.totalizer_drain_input_step
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(a : T)
(w : List T)
(top : TotalStackSymbol A)
(rest : List (TotalStackSymbol A))
:
PDA.Reaches₁ { state := TotalState.drain, input := a :: w, stack := top :: rest }
{ state := TotalState.drain, input := w, stack := top :: rest }
theorem
DPDA.totalizer_drain_reaches_empty_input
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(w : List T)
(top : TotalStackSymbol A)
(rest : List (TotalStackSymbol A))
:
PDA.Reaches { state := TotalState.drain, input := w, stack := top :: rest }
{ state := TotalState.drain, input := [], stack := top :: rest }
theorem
DPDA.totalizer_no_transition_reaches_empty_drain
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q : Q}
{b : Bool}
{a : T}
{Z : S}
{below : AnalysisSummary A}
{rest : List (TotalStackSymbol A)}
{w : List T}
(hε : M.epsilon_transition q Z = none)
(hδ : M.transition q a Z = none)
:
theorem
DPDA.totalizer_stable_input_step_preserves_annotations
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q p : Q}
{b : Bool}
{a : T}
{Z : S}
{below : AnalysisSummary A}
{β : List S}
{rest : List (TotalStackSymbol A)}
{w : List T}
(hstack : StackWellAnnotated A (some (Z, below) :: rest))
(hbottom : StackHasBottom A (some (Z, below) :: rest))
(hstable : M.EpsilonStable (q, eraseAnnotatedStack A (some (Z, below) :: rest)))
(hδ : M.transition q a Z = some (p, β))
:
∃ (stack' : List (TotalStackSymbol A)) (summary' : AnalysisSummary A),
PDA.Reaches₁ { state := TotalState.sim q b, input := a :: w, stack := some (Z, below) :: rest }
{ state := simState A p summary', input := w, stack := stack' } ∧ StackWellAnnotated A stack' ∧ StackHasBottom A stack' ∧ SummaryRepresents A summary' (eraseAnnotatedStack A stack') ∧ eraseAnnotatedStack A stack' = β ++ eraseAnnotatedStack A rest
theorem
DPDA.totalizer_stable_no_transition_reaches_empty_drain
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q : Q}
{b : Bool}
{a : T}
{Z : S}
{below : AnalysisSummary A}
{rest : List (TotalStackSymbol A)}
{w : List T}
(hstable : M.EpsilonStable (q, eraseAnnotatedStack A (some (Z, below) :: rest)))
(hδ : M.transition q a Z = none)
:
theorem
DPDA.totalizer_unstopping_epsilon_reaches_empty_drain
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q p : Q}
{b : Bool}
{a : T}
{Z : S}
{below : AnalysisSummary A}
{β : List S}
{rest : List (TotalStackSymbol A)}
{w : List T}
(hε : M.epsilon_transition q Z = some (p, β))
(hstop : ¬stopsFromSummary A q (fullSummaryOfTop A (some (Z, below))))
:
theorem
DPDA.totalizer_empty_original_stack_reaches_empty_drain
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
{q : Q}
{b : Bool}
{a : T}
{rest : List (TotalStackSymbol A)}
{w : List T}
:
PDA.Reaches { state := TotalState.sim q b, input := a :: w, stack := none :: rest }
{ state := TotalState.drain, input := [], stack := none :: rest }
theorem
DPDA.totalizer_reaches_empty_from_sim
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(q : Q)
(b : Bool)
(w : List T)
(top : TotalStackSymbol A)
(rest : List (TotalStackSymbol A))
(hstack : StackWellAnnotated A (top :: rest))
(hbottom : StackHasBottom A (top :: rest))
:
∃ (st : TotalState Q) (stack : List (TotalStackSymbol A)),
PDA.Reaches { state := TotalState.sim q b, input := w, stack := top :: rest }
{ state := st, input := [], stack := stack }
theorem
DPDA.totalizer_accepting_reaches_from_simState
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(q : Q)
(w : List T)
(top : TotalStackSymbol A)
(rest : List (TotalStackSymbol A))
(hstack : StackWellAnnotated A (top :: rest))
(hbottom : StackHasBottom A (top :: rest))
{qf : Q}
{γf : List S}
(hreach :
PDA.Reaches { state := q, input := w, stack := eraseAnnotatedStack A (top :: rest) }
{ state := qf, input := [], stack := γf })
(hqf : qf ∈ M.final_states)
:
∃ (st : TotalState Q) (stack : List (TotalStackSymbol A)),
PDA.Reaches { state := simState A q (fullSummaryOfTop A top), input := w, stack := top :: rest }
{ state := st, input := [], stack := stack } ∧ st ∈ (totalizer A).final_states
theorem
DPDA.totalizer_reaches_empty
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(w : List T)
:
∃ (st : TotalState Q) (stack : List (TotalStackSymbol A)),
PDA.Reaches { state := (totalizer A).initial_state, input := w, stack := [(totalizer A).start_symbol] }
{ state := st, input := [], stack := stack }
theorem
DPDA.original_accept_subset_totalizer_acceptsByFinalState
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
theorem
DPDA.totalizer_acceptsByFinalState_eq_original
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
:
theorem
DPDA.totalizer_total
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(w : List T)
:
∃ (st : TotalState Q) (stack : List (TotalStackSymbol A)),
PDA.Reaches { state := (totalizer A).initial_state, input := w, stack := [(totalizer A).start_symbol] }
{ state := st, input := [], stack := stack }
theorem
DPDA.totalizer_final_consistent
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
(w : List T)
(st₁ st₂ : TotalState Q)
(stack₁ stack₂ : List (TotalStackSymbol A))
(h₁ :
PDA.Reaches { state := (totalizer A).initial_state, input := w, stack := [(totalizer A).start_symbol] }
{ state := st₁, input := [], stack := stack₁ })
(h₂ :
PDA.Reaches { state := (totalizer A).initial_state, input := w, stack := [(totalizer A).start_symbol] }
{ state := st₂, input := [], stack := stack₂ })
:
theorem
DPDA.totalizer_decides
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : DPDA Q T S}
(A : M.RegularEpsilonAnalysis)
: