Langlib

Langlib.Automata.LinearBounded.CertifiedRowSystem.Complement.EnumerationScannerCorrectness

Correctness of the enumeration-action scanners #

This file connects the finite-state scanners in EnumerationScanners.lean to the declarative list-level specifications in EnumerationActions.lean.

source
def CertifiedRowSystem.Complement.EnumerationAccepts {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (action : ProtocolAction) (old new : ProtocolRow A) :
Prop

Acceptance of one action repeated across the complete certificate row.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CertifiedRowSystem.Complement.enumerationAccepts_beginRound_iff {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (old new : ProtocolRow A) :
    EnumerationAccepts ProtocolAction.beginRound old new ↔ old ≠ [] ∧ BeginRoundSpec old new

    Correctness of the transition entering an inner enumeration round.

    source
    @[simp]
    theorem CertifiedRowSystem.Complement.enumerationAccepts_skipInner_iff {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (old new : ProtocolRow A) :
    EnumerationAccepts ProtocolAction.skipInner old new ↔ old ≠ [] ∧ SkipInnerSpec old new

    Correctness of one canonical inner-enumeration successor.

    source
    @[simp]
    theorem CertifiedRowSystem.Complement.enumerationAccepts_finalFinish_iff {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (old new : ProtocolRow A) :
    EnumerationAccepts ProtocolAction.finalFinish old new ↔ old ≠ [] ∧ FinalFinishSpec old new

    Correctness of the accepting transition after the final enumeration.

    source
    @[simp]
    theorem CertifiedRowSystem.Complement.enumerationAccepts_finalSkip_iff {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (old new : ProtocolRow A) :
    EnumerationAccepts ProtocolAction.finalSkip old new ↔ old ≠ [] ∧ FinalSkipSpec old new

    Correctness of one canonical successor in the final scan.

    source
    @[simp]
    theorem CertifiedRowSystem.Complement.enumerationAccepts_finishOuter_iff {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (old new : ProtocolRow A) :
    EnumerationAccepts ProtocolAction.finishOuter old new ↔ old ≠ [] ∧ FinishOuterSpec old new

    Correctness of classifying one outer vertex and advancing its enumeration.

    source
    @[simp]
    theorem CertifiedRowSystem.Complement.enumerationAccepts_finishRound_iff {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (old new : ProtocolRow A) :
    EnumerationAccepts ProtocolAction.finishRound old new ↔ old ≠ [] ∧ FinishRoundSpec old new

    Correctness of the boundary between two counting rounds, including plateau detection and the non-plateau depth successor.