OAI/Combinatorics/ContingencyTables/Machines/OnlinePartialCall.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.OnlinePartialCall.embed line 15
2. def OAI.ContingencyTables.OnlinePartialCall.callCfg line 18
3. theorem OAI.ContingencyTables.OnlinePartialCall.partial_call line 24

   Source documentation

   A finite prefix of a called procedure can end at a live internal label. Only actual halts return to the continuation label.

   theorem partial_call (M : Λ → Instr R Λ) (l : Λ)
       (hcall : ∃ P next, M l = .call P next) (E : Env R)
       (out : α → TM2.Cfg (fun _ : K R => Bool) (procedure (M l)).Label RegisterProc.Store)
       (p : Experiment α)
       (hp : Executes (procedure (M l)).code (procedure (M l)).coin out
         ⟨some default,none,encodeEnv E⟩ p) :
       Executes (code M) (coins M) (fun a => callCfg M l (out a))
         (OnlineControl.cfg M (some l) E) (.delay 1 p) := by
   …

   Mentions: OAI.ContingencyTables.OnlinePartialCall.call, OAI.ContingencyTables.OnlinePartialCall.callCfg

4. abbrev OAI.ContingencyTables.OnlinePartialCall.Config line 38
5. def OAI.ContingencyTables.OnlinePartialCall.At line 41
6. lemma OAI.ContingencyTables.OnlinePartialCall.halt line 45
7. lemma OAI.ContingencyTables.OnlinePartialCall.nilBranch line 54
8. lemma OAI.ContingencyTables.OnlinePartialCall.consBranch line 62
9. lemma OAI.ContingencyTables.OnlinePartialCall.call line 70
10. lemma OAI.ContingencyTables.OnlinePartialCall.deterministicCall line 88