OAI/Combinatorics/UniformKServer/LiteralPartrec.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.UniformKServer.LiteralPartrec.(instance at line 12) line 12
2. theorem OAI.UniformKServer.LiteralPartrec.code_exists line 16

   Source documentation

   A fixed Partrec program has one fixed finite-control literal processor. Its parameter is supplied on a stack, not hidden in the transition table.

   theorem code_exists {α β : Type} [Primcodable α] [Primcodable β]
       (f : α→.β) (hf : Partrec f) :
       ∃c : Code,∀a b,b ∈ f a → ([Encodable.encode b] : List ℕ) ∈ Code.eval c [Encodable.encode a] := by
   …

3. def OAI.UniformKServer.LiteralPartrec.supp line 34
4. def OAI.UniformKServer.LiteralPartrec.processor line 36
5. def OAI.UniformKServer.LiteralPartrec.input line 41
6. theorem OAI.UniformKServer.LiteralPartrec.halts line 47