OAI/Computability/Interspersed/Erasure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Erasure of retained history symbols from work stacks.

  1. inductive OAI.PrefixFlows.Interspersed.Erases line 13
  2. theorem OAI.PrefixFlows.Interspersed.Erases.work_inv line 23
  3. theorem OAI.PrefixFlows.Interspersed.Erases.record_inv line 43
  4. theorem OAI.PrefixFlows.Interspersed.Erases.prepend_records line 57
  5. theorem OAI.PrefixFlows.Interspersed.Erases.of_prepend_records line 63
  6. theorem OAI.PrefixFlows.Interspersed.Erases.prepend_work line 69
  7. theorem OAI.PrefixFlows.Interspersed.Erases.eventually_blank line 77
  8. theorem OAI.PrefixFlows.Interspersed.Erases.eq_blank line 89
  9. theorem OAI.PrefixFlows.Interspersed.Erases.deterministic line 106