OAI/Computability/WitnessedChoice/CumulativeEvaluation.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.WitnessedSeparation.FullCPT.Term line 16
  2. def OAI.WitnessedSeparation.FullCPT.Term.eval line 41
  3. def OAI.WitnessedSeparation.FullCPT.bindSlots line 66
  4. def OAI.WitnessedSeparation.FullCPT.Agrees line 69
  5. lemma OAI.WitnessedSeparation.FullCPT.agrees_bind line 73
  6. def OAI.WitnessedSeparation.FullCPT.Term.compile line 87
  7. theorem OAI.WitnessedSeparation.FullCPT.Term.eval_compile line 110
  8. inductive OAI.WitnessedSeparation.FullCPT.Rule line 156
  9. def OAI.WitnessedSeparation.FullCPT.Rule.updates line 166
  10. def OAI.WitnessedSeparation.FullCPT.Rule.compile line 176
  11. theorem OAI.WitnessedSeparation.FullCPT.Rule.updates_compile line 184
  12. structure OAI.WitnessedSeparation.FullCPT.Program line 208
  13. abbrev OAI.WitnessedSeparation.FullCPT.Program.functionArity line 218
  14. abbrev OAI.WitnessedSeparation.FullCPT.Program.Store line 220
  15. def OAI.WitnessedSeparation.FullCPT.Program.flag line 222
  16. def OAI.WitnessedSeparation.FullCPT.Program.step line 224
  17. def OAI.WitnessedSeparation.FullCPT.Program.run line 229
  18. def OAI.WitnessedSeparation.FullCPT.Program.active line 233
  19. def OAI.WitnessedSeparation.FullCPT.Program.accepts line 236
  20. def OAI.WitnessedSeparation.FullCPT.Program.compile line 240
  21. lemma OAI.WitnessedSeparation.FullCPT.Program.flag_compile line 247
  22. lemma OAI.WitnessedSeparation.FullCPT.Program.step_compile line 249
  23. lemma OAI.WitnessedSeparation.FullCPT.Program.run_compile line 260
  24. lemma OAI.WitnessedSeparation.FullCPT.Program.active_compile line 270
  25. lemma OAI.WitnessedSeparation.FullCPT.Program.accepts_compile line 278
  26. def OAI.WitnessedSeparation.FullCPT.Definable line 286
  27. theorem OAI.WitnessedSeparation.FullCPT.query_not_definable line 290
  28. abbrev OAI.WitnessedSeparation.Operational.Machine.Observer line 313
  29. abbrev OAI.WitnessedSeparation.Operational.Machine.instrument line 315
  30. lemma OAI.WitnessedSeparation.Operational.Machine.instrument_step line 323
  31. lemma OAI.WitnessedSeparation.Operational.Machine.instrument_run line 328
  32. lemma OAI.WitnessedSeparation.Operational.Machine.instrument_active line 338
  33. lemma OAI.WitnessedSeparation.Operational.Machine.observer_trace_subset line 345
  34. lemma OAI.WitnessedSeparation.Operational.Machine.original_trace_subset line 350
  35. def OAI.WitnessedSeparation.Operational.Machine.observed line 353
  36. lemma OAI.WitnessedSeparation.Operational.Machine.observed_subset_trace line 358
  37. lemma OAI.WitnessedSeparation.Operational.Machine.active_subset_observed line 376
  38. lemma OAI.WitnessedSeparation.Operational.Term.uniform_root_members line 416
  39. lemma OAI.WitnessedSeparation.Operational.Machine.uniform_observed line 484
  40. lemma OAI.WitnessedSeparation.Grid.op_observed_agrees line 542
  41. def OAI.WitnessedSeparation.Operational.Machine.observedAccepts line 633
  42. lemma OAI.WitnessedSeparation.Operational.Machine.observed_implies_bounded line 637
  43. lemma OAI.WitnessedSeparation.Operational.Machine.observed_accept_transfer line 648
  44. lemma OAI.WitnessedSeparation.Operational.Machine.observed_accept_iff line 679
  45. def OAI.WitnessedSeparation.Operational.Machine.polynomialObservedAccepts line 697
  46. lemma OAI.WitnessedSeparation.Operational.Machine.observedAccepts_fintype line 701
  47. lemma OAI.WitnessedSeparation.Grid.op_prefix_observed line 724
  48. theorem OAI.WitnessedSeparation.Grid.polynomial_observed_agrees_on_some_box line 758
  49. theorem OAI.WitnessedSeparation.query_not_polynomial_observed_HF line 852