OAI/Combinatorics/UniformKServer/FlatTermination.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.FlatTM2.fromCfg line 15
2. theorem OAI.UniformKServer.FlatTM2.advances_aux line 20

   Source documentation

   Every Mathlib TM2 macro-step is a finite sequence of literal primitives.

   theorem advances_aux (q : TM2.Stmt (fun _ : K=>Γ) Λ V) (v : V) (st : K → List Γ) :
       ∃t : ℕ,(advance M)^[t] ⟨some q,v,st⟩=fromCfg M (TM2.stepAux q v st) := by
   …

   Mentions: OAI.UniformKServer.FlatTM2.advance, OAI.UniformKServer.FlatTM2.fromCfg

3. theorem OAI.UniformKServer.FlatTM2.advances_step line 47
4. theorem OAI.UniformKServer.FlatTM2.advances_reaches line 58
5. theorem OAI.UniformKServer.FlatTM2.iterate_supported line 69
6. theorem OAI.UniformKServer.FlatTM2.encode_run line 77
7. theorem OAI.UniformKServer.FlatTM2.fromCfg_supported line 88
8. theorem OAI.UniformKServer.FlatTM2.processor_halts line 96

   Source documentation

   Halting is inherited by the actual finite-control stack processor.

   theorem processor_halts (v₀ : V) (c c' : TM2.Cfg (fun _ : K=>Γ) Λ V)
       (hc : c.l∈Finset.insertNone S) (h : TM2.Reaches M c c') (hhalt : c'.l=none) :
       ∃t : ℕ, (run (processor M S hs v₀)
         (encode M S (fromCfg M c) (fromCfg_supported M S c hc)) (List.replicate t false)).yielded=true ∧
         ∀i, (run (processor M S hs v₀)
         (encode M S (fromCfg M c) (fromCfg_supported M S c hc)) (List.replicate t false)).store i=
           (c'.stk (keys.symm i)).map letters := by
   …

   Mentions: OAI.UniformKServer.FlatTM2.processor, OAI.UniformKServer.FlatTM2.encode, OAI.UniformKServer.FlatTM2.fromCfg, OAI.UniformKServer.FlatTM2.fromCfg_supported, OAI.UniformKServer.FlatTM2.letters