OAI/ModelTheory/Choiceless/Observers.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CPTSeparation.Operational.Machine.Observer line 15
  2. abbrev OAI.CPTSeparation.Operational.Machine.instrument line 17
  3. lemma OAI.CPTSeparation.Operational.Machine.instrument_step line 25
  4. lemma OAI.CPTSeparation.Operational.Machine.instrument_run line 30
  5. lemma OAI.CPTSeparation.Operational.Machine.instrument_active line 40
  6. lemma OAI.CPTSeparation.Operational.Machine.observer_trace_subset line 47
  7. lemma OAI.CPTSeparation.Operational.Machine.original_trace_subset line 52
  8. def OAI.CPTSeparation.Operational.Machine.observed line 55
  9. lemma OAI.CPTSeparation.Operational.Machine.observed_subset_trace line 60
  10. lemma OAI.CPTSeparation.Operational.Machine.active_subset_observed line 78
  11. lemma OAI.CPTSeparation.Operational.Term.uniform_root_members line 112
  12. lemma OAI.CPTSeparation.Operational.Machine.uniform_observed line 174
  13. lemma OAI.CPTSeparation.Grid.op_observed_agrees line 226
  14. def OAI.CPTSeparation.Operational.Machine.observedAccepts line 313
  15. lemma OAI.CPTSeparation.Operational.Machine.observed_implies_bounded line 317
  16. lemma OAI.CPTSeparation.Operational.Machine.observed_accept_transfer line 328
  17. lemma OAI.CPTSeparation.Operational.Machine.observed_accept_iff line 359
  18. def OAI.CPTSeparation.Operational.Machine.polynomialObservedAccepts line 371
  19. lemma OAI.CPTSeparation.Operational.Machine.observedAccepts_fintype line 375
  20. lemma OAI.CPTSeparation.Grid.op_prefix_observed line 394
  21. theorem OAI.CPTSeparation.Grid.polynomial_observed_agrees_on_some_box line 422
  22. theorem OAI.CPTSeparation.query_not_polynomial_observed_HF line 512