OAI/Computability/WLIdentification/WordCommands.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WLIdentification.StackModel.Command.read line 11
2. abbrev OAI.WLIdentification.StackModel.Command.emit line 12
3. def OAI.WLIdentification.StackModel.Command.drain line 14
4. def OAI.WLIdentification.StackModel.Command.clear line 17
5. def OAI.WLIdentification.StackModel.Command.move line 19
6. theorem OAI.WLIdentification.StackModel.Command.drain_exec line 22

   Source documentation

   Tail traversal is an actual structured loop, not a host-language iteration.

   theorem drain_exec (k : K) (body : Command K (Option Bool))
       (S : K → Word) (s : Option Bool) (f : Bool → (K → Word) → (K → Word)) (c : ℕ)
       (hbody : ∀ b T, ∃ t, Exec body (some b) T t (f b T) c)
       (hpres : ∀ b T, f b T k = T k) :
       ∃ n ≤ (c + 2) * (S k).length + 2,
         Exec (drain k body) s S none
           ((S k).reverse.foldl (fun T b => f b (Function.update T k (T k).dropLast))
             S) n := by
   …

   Mentions: OAI.WLIdentification.StackModel.Command, OAI.WLIdentification.Word, OAI.WLIdentification.StackModel.Command.Exec, OAI.WLIdentification.StackModel.Command.drain

7. def OAI.WLIdentification.StackModel.Command.pushMany line 67
8. def OAI.WLIdentification.StackModel.Command.appendMany line 70
9. theorem OAI.WLIdentification.StackModel.Command.pushMany_exec line 73
10. def OAI.WLIdentification.StackModel.Command.fanEffect line 91
11. theorem OAI.WLIdentification.StackModel.Command.fan_fold line 94
12. theorem OAI.WLIdentification.StackModel.Command.fan_exec line 116
13. theorem OAI.WLIdentification.StackModel.Command.clear_exec line 126
14. theorem OAI.WLIdentification.StackModel.Command.move_exec line 134
15. def OAI.WLIdentification.StackModel.Command.copy line 147

    Source documentation

    Copy a complete word, preserving its order and the source, using one private work stack.

    def copy (a b tmp : K) : Command K (Option Bool) :=
    …

    Mentions: OAI.WLIdentification.StackModel.Command

16. theorem OAI.WLIdentification.StackModel.Command.copy_exec line 151
17. def OAI.WLIdentification.StackModel.Command.rename line 185
18. theorem OAI.WLIdentification.StackModel.Command.rename_rename line 194
19. theorem OAI.WLIdentification.StackModel.Command.Exec.rename line 201

    Source documentation

    Renaming uses only the named stacks; arbitrary ambient data are framed.

    theorem Exec.rename {c : Command K R} {s S t T n} (h : Exec c s S t T n)
        (e : K ↪ L) (W : L → Word) (hW : W ∘ e = S) :
        ∃ U, Exec (c.rename e) s W t U n ∧ U ∘ e = T ∧
          ∀ l, (∀ k, e k ≠ l) → U l = W l := by
    …

    Mentions: OAI.WLIdentification.StackModel.Command, OAI.WLIdentification.StackModel.Command.Exec, OAI.WLIdentification.Word

20. def OAI.WLIdentification.StackModel.Command.embedLeft line 241
21. def OAI.WLIdentification.StackModel.Command.embedRight line 251
22. theorem OAI.WLIdentification.StackModel.Command.Exec.left line 261
23. theorem OAI.WLIdentification.StackModel.Command.Exec.right line 276
24. theorem OAI.WLIdentification.StackModel.Command.while_steps line 292

    Source documentation

    A finite chain of loop states has the counted actual execution.

    theorem while_steps (test : R → Bool) (c : Command K R) (n cost : ℕ)
        (s : ℕ → R) (S : ℕ → K → Word)
        (hs : ∀ i < n, test (s i) = true) (hn : test (s n) = false)
        (hstep : ∀ i < n, ∃ t ≤ cost, Exec c (s i) (S i) (s (i+1)) (S (i+1)) t) :
        ∃ t ≤ (cost + 1) * n + 1, Exec (.while test c) (s 0) (S 0) (s n) (S n) t := by
    …

    Mentions: OAI.WLIdentification.StackModel.Command, OAI.WLIdentification.Word, OAI.WLIdentification.StackModel.Command.Exec