Research source · Plain text

FPRDTransfer.lean

site/public/formal/persistent-stacks/lean/FPRDTransfer.lean

22 lines. Source is displayed for inspection; it is not executed by this page.

File fingerprint

SHA-256: 4406d3eca14f5410f5d943470de211fa65b9308222402810192209a21c735001

import FPRDTransfer.LMR
import FPRDTransfer.FiniteEnum
import FPRDTransfer.PEG.Syntax
import FPRDTransfer.PEG.Semantics
import FPRDTransfer.PEG.Examples
import FPRDTransfer.PEG.TableEval
import FPRDTransfer.PEG.TableEvalExamples
import FPRDTransfer.Theorem16.Normalize
import FPRDTransfer.Theorem16.Reachability
import FPRDTransfer.Theorem16.Grammar
import FPRDTransfer.Theorem16.Invariants.StateLabel
import FPRDTransfer.Theorem16.Invariants.Path
import FPRDTransfer.Theorem16.Invariants.Neighbourhood
import FPRDTransfer.Theorem16.Main
import FPRDTransfer.Theorem16.Corollaries
import FPRDTransfer.Theorem16.FixtureAudit
import FPRDTransfer.StackMachine
import FPRDTransfer.StackEncoding
import FPRDTransfer.Compile
import FPRDTransfer.TapeZipper
import FPRDTransfer.RealtimeTransfer
import FPRDTransfer.Example