OAI/Computability/WitnessedChoice/LowerBound.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WitnessedSeparation.Operational.State.mem_critical_iff line 35
  2. lemma OAI.WitnessedSeparation.Operational.State.uniform_critical line 48
  3. def OAI.WitnessedSeparation.Operational.State.rootFamily line 94
  4. lemma OAI.WitnessedSeparation.Operational.State.uniform_roots line 98
  5. lemma OAI.WitnessedSeparation.Operational.State.uniform_descendants line 121
  6. lemma OAI.WitnessedSeparation.Operational.State.uniform_active line 141
  7. lemma OAI.WitnessedSeparation.Operational.State.uniform_active_card line 154
  8. lemma OAI.WitnessedSeparation.Operational.uniform_consistency line 191
  9. lemma OAI.WitnessedSeparation.Grid.op_observations_agree line 239
  10. lemma OAI.WitnessedSeparation.Operational.State.active_apply_subset line 335
  11. lemma OAI.WitnessedSeparation.Operational.State.initial_active_card line 370
  12. def OAI.WitnessedSeparation.Operational.Machine.boundedAccepts line 411
  13. lemma OAI.WitnessedSeparation.Operational.Machine.step_exists_iff line 415
  14. lemma OAI.WitnessedSeparation.Operational.Machine.active_step_bound line 423
  15. def OAI.WitnessedSeparation.Operational.Machine.PrefixBound line 460
  16. def OAI.WitnessedSeparation.Operational.Machine.ObservationsAt line 463
  17. lemma OAI.WitnessedSeparation.Operational.Machine.bounded_accept_transfer line 470
  18. lemma OAI.WitnessedSeparation.Operational.Machine.bounded_accept_iff line 557
  19. lemma OAI.WitnessedSeparation.Grid.op_prefix_observations line 579
  20. lemma OAI.WitnessedSeparation.PolynomialCost.eval_mono line 616
  21. def OAI.WitnessedSeparation.Operational.Machine.cutoffAccepts line 628
  22. lemma OAI.WitnessedSeparation.Grid.atom_card_independent line 646
  23. lemma OAI.WitnessedSeparation.Operational.Machine.boundedAccepts_fintype line 669
  24. theorem OAI.WitnessedSeparation.Grid.cutoff_agrees_on_some_box line 687
  25. theorem OAI.WitnessedSeparation.query_not_cutoff_HF line 752
  26. lemma OAI.WitnessedSeparation.Operational.Machine.uniform_runActive line 792
  27. lemma OAI.WitnessedSeparation.Operational.Machine.uniform_finite_family_card line 818
  28. lemma OAI.WitnessedSeparation.Grid.op_cumulative_agrees line 851
  29. def OAI.WitnessedSeparation.Operational.Machine.cumulativeAccepts line 919
  30. lemma OAI.WitnessedSeparation.Operational.Machine.cumulative_implies_bounded line 923
  31. lemma OAI.WitnessedSeparation.Operational.Machine.bounded_active_all line 930
  32. lemma OAI.WitnessedSeparation.Operational.Machine.cumulative_accept_transfer line 944
  33. lemma OAI.WitnessedSeparation.Operational.Machine.cumulative_accept_iff line 975
  34. def OAI.WitnessedSeparation.Operational.Machine.cumulativeCutoffAccepts line 992
  35. lemma OAI.WitnessedSeparation.Grid.op_prefix_cumulative line 1010
  36. lemma OAI.WitnessedSeparation.Operational.Machine.cumulativeAccepts_fintype line 1039
  37. theorem OAI.WitnessedSeparation.Grid.cumulative_cutoff_agrees_on_some_box line 1057
  38. theorem OAI.WitnessedSeparation.query_not_cumulative_cutoff_HF line 1127
  39. def OAI.WitnessedSeparation.Operational.Machine.polynomialCumulativeAccepts line 1142
  40. theorem OAI.WitnessedSeparation.Grid.polynomial_cumulative_agrees_on_some_box line 1158
  41. theorem OAI.WitnessedSeparation.query_not_polynomial_cumulative_HF line 1242