Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

The wide problems, characterized

Lax822549.WideProblemsValues · concepts/Lax822549/WideProblemsValues.lean · lax-822549

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    The conditions of the wide machine and tiling problems are invariant under isomorphism of instances, so each problem holds of an instance exactly when its conditions do.

    Concept map
    22 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 6 statements. Each proof establishes one of them relative to its assumptions.

    1 dwideAcceptSpace_iff proven

    2 wideAccept_iff proven

    3 wideAcceptSpace_iff proven

    4 wideCorridor_iff proven

    5 wideRegAccept_iff proven

    6 wideTiling_iff proven

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax904597.Classes
    3import Lax904597.Machines
    4import Lax485149.Problems
    5import Lax535992.DeterministicMachines
    6import Lax134656.SpaceBoundedMachines
    7import Lax480241.ExponentialClasses
    8import Lax822549.WideMachines
    9import Lax822549.WideRegChannel
    10import Lax822549.WideTilings
    11
    12/-!
    13---
    14title: The wide problems, characterized
    15type: lemma
    16---
    17The conditions of the wide machine and tiling problems are invariant under
    18isomorphism of instances, so each problem holds of an instance exactly when
    19its conditions do.
    20-/
    21
    22namespace Lax822549.WideProblemsValues
    23
    24open FirstOrder FirstOrder.Language
    25open Lax904597.Problems Lax904597.Classes Lax904597.Machines Lax485149.Problems
    26 Lax480241.ExponentialClasses
    27open Lax822549.WideMachines Lax822549.WideRegChannel Lax822549.WideTilings
    28
    29/-- The problem holds exactly when its conditions do. -/
    30axiom wideAccept_iff :
    31 ∀ (A : Type) [wide.Structure A],
    32 WideAccept A ↔ TMData.WellFormed (wideData A) ∧ TMData.Accepts (wideData A)
    33
    34/-- The problem holds exactly when its conditions do. -/
    35axiom wideAcceptSpace_iff :
    36 ∀ (A : Type) [wide.Structure A],
    37 WideAcceptSpace A ↔ TMData.WellFormed (wideData A) ∧
    38 Lax134656.SpaceBoundedMachines.TMData.AcceptsSpace (wideData A)
    39
    40/-- The problem holds exactly when its conditions do. -/
    41axiom dwideAcceptSpace_iff :
    42 ∀ (A : Type) [wide.Structure A],
    43 DWideAcceptSpace A ↔ TMData.WellFormed
    44 (wideData A) ∧ Lax535992.DeterministicMachines.TMData.Deterministic (wideData A) ∧
    45 Lax134656.SpaceBoundedMachines.TMData.AcceptsSpace (wideData A)
    46
    47/-- The problem holds exactly when its conditions do. -/
    48axiom wideRegAccept_iff :
    49 ∀ (A : Type) [wide.Structure A],
    50 WideRegAccept A ↔ TMData.WellFormed (wideRegData A) ∧ TMData.Accepts (wideRegData A)
    51
    52/-- The problem holds exactly when its conditions do. -/
    53axiom wideTiling_iff :
    54 ∀ (A : Type) [wtile.Structure A],
    55 WideTiling A ↔ (wideTileData A).WellFormed ∧ (wideTileData A).Tileable
    56
    57/-- The problem holds exactly when its conditions do. -/
    58axiom wideCorridor_iff :
    59 ∀ (A : Type) [wtile.Structure A],
    60 WideCorridor A ↔ (wideTileData A).WellFormed ∧ (wideTileData A).CorridorTileable
    61
    62end Lax822549.WideProblemsValues
    63
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…