OAI/Computability/RationalHitting/OutputComputation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RationalHitting.StackLanguage.unaryScanBody line 10

   Source documentation

   Strip the one literal separator of the required unary input, remembering its first field in a separate finite stack.

   def unaryScanBody : Program (Fin 3) :=
   …

   Mentions: OAI.RationalHitting.StackLanguage.Program

2. def OAI.RationalHitting.StackLanguage.unaryScan line 13
3. lemma OAI.RationalHitting.StackLanguage.eval_unaryScan line 15
4. def OAI.RationalHitting.StackLanguage.Procedure.unaryInput line 57

   Source documentation

   A fixed three-stack parser for the literal, unescaped unary input. Its output is the ordinary typed pair coding used by the closure library.

   def unaryInput : Procedure
       (fun a : ℕ×ℕ => ExecutableGenerator.unaryWord a.1 a.2)
       (code : Unary×Unary → List Bool) (fun a => (Unary.mk a.1,Unary.mk a.2)) where
   …

   Mentions: OAI.RationalHitting.StackLanguage.Procedure, OAI.RationalHitting.ExecutableGenerator.unaryWord, OAI.RationalHitting.StackLanguage.Unary

5. def OAI.RationalHitting.StackLanguage.Runtime.word line 98

   Source documentation

   Literal canonical output, including dimension and accepted-list length.

   def word (p : Params) : BitWord :=
   …

   Mentions: OAI.RationalHitting.StackLanguage.Params, OAI.RationalHitting.StackLanguage.BitWord

6. theorem OAI.RationalHitting.StackLanguage.Runtime.word_poly line 101
7. lemma OAI.RationalHitting.StackLanguage.Runtime.word_eq line 108
8. lemma OAI.RationalHitting.StackLanguage.Runtime.word_ext line 114
9. theorem OAI.RationalHitting.StackLanguage.Runtime.output_poly line 117
10. theorem OAI.RationalHitting.StackLanguage.Runtime.raw_feasible line 123

    Source documentation

    Polynomial feasibility of the canonical output construction.

    theorem raw_feasible : Feasible
        (fun a : ℕ×ℕ => ExecutableGenerator.unaryWord a.1 a.2)
        _root_.id (fun a => (ExecutableGenerator.encoded a.1 a.2).reverse) := by
    …

    Mentions: OAI.RationalHitting.StackLanguage.Feasible, OAI.RationalHitting.ExecutableGenerator.unaryWord, OAI.RationalHitting.ExecutableGenerator.encoded, OAI.RationalHitting.StackLanguage.reverse