OAI/Computability/WLIdentification/TapeCompiler.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WLIdentification.StackModel.push_at_end line 11
2. theorem OAI.WLIdentification.StackModel.push_execution line 24
3. theorem OAI.WLIdentification.StackModel.ready_push line 32
4. theorem OAI.WLIdentification.StackModel.ready_push_execution line 40
5. theorem OAI.WLIdentification.StackModel.pop_at_end line 49
6. theorem OAI.WLIdentification.StackModel.read_empty line 58
7. theorem OAI.WLIdentification.StackModel.tape_pop line 65
8. theorem OAI.WLIdentification.StackModel.read_last line 84
9. theorem OAI.WLIdentification.StackModel.pop_execution line 96
10. theorem OAI.WLIdentification.StackModel.ready_pop line 123
11. theorem OAI.WLIdentification.StackModel.ready_pop_execution line 130
12. def OAI.WLIdentification.StackModel.encodeConfig line 146
13. theorem OAI.WLIdentification.StackModel.initial_tape line 153
14. theorem OAI.WLIdentification.StackModel.initial_execution line 179
15. theorem OAI.WLIdentification.StackModel.instruction_execution line 215

    Source documentation

    Uniform interpreter cost for one instruction, including all scans.

    theorem instruction_execution (c : Config K Λ R) (n : ℕ)
        (hn : ∀ k, (c.stk k).length ≤ n) :
        ∃ t ≤ 2 * n + 3, (WLIdentification.step (compile P input))^[t]
          (encodeConfig P input c) = encodeConfig P input (step P c) := by
    …

    Mentions: OAI.WLIdentification.StackModel.Config, OAI.WLIdentification.step, OAI.WLIdentification.StackModel.compile, OAI.WLIdentification.StackModel.encodeConfig, OAI.WLIdentification.StackModel.step

16. theorem OAI.WLIdentification.StackModel.step_length line 252
17. theorem OAI.WLIdentification.StackModel.run_length line 272
18. theorem OAI.WLIdentification.StackModel.run_execution line 284

    Source documentation

    The compilation preserves a real execution with a quadratic simulation bound.

    theorem run_execution (w : Word) (t : ℕ) :
        ∃ T ≤ 2 + t * (2 * (w.length + t) + 3),
          WLIdentification.run (compile P input) w T = encodeConfig P input (run P input w t) := by
    …

    Mentions: OAI.WLIdentification.Word, OAI.WLIdentification.run, OAI.WLIdentification.StackModel.compile, OAI.WLIdentification.StackModel.encodeConfig, OAI.WLIdentification.StackModel.run

19. theorem OAI.WLIdentification.StackModel.output_correct line 299

    Source documentation

    Only the input track is present at output; the fixed marker is at negative position.

    theorem output_correct (c : Config K Λ R) (w : Word)
        (h : c.stk = Function.update (fun _ => []) input w) :
        Output (encodeConfig P input c) w := by
    …

    Mentions: OAI.WLIdentification.StackModel.Config, OAI.WLIdentification.Word, OAI.WLIdentification.Output, OAI.WLIdentification.StackModel.encodeConfig