OAI/ModelTheory/Choiceless/LowerBound.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CPTSeparation.query_not_cutoff_HF line 9
  2. lemma OAI.CPTSeparation.Operational.Machine.uniform_runActive line 46
  3. lemma OAI.CPTSeparation.Operational.Machine.uniform_finite_family_card line 72
  4. lemma OAI.CPTSeparation.Grid.op_cumulative_agrees line 108
  5. def OAI.CPTSeparation.Operational.Machine.cumulativeAccepts line 173
  6. lemma OAI.CPTSeparation.Operational.Machine.cumulative_implies_bounded line 177
  7. lemma OAI.CPTSeparation.Operational.Machine.bounded_active_all line 184
  8. lemma OAI.CPTSeparation.Operational.Machine.cumulative_accept_transfer line 198
  9. lemma OAI.CPTSeparation.Operational.Machine.cumulative_accept_iff line 229
  10. def OAI.CPTSeparation.Operational.Machine.cumulativeCutoffAccepts line 241
  11. lemma OAI.CPTSeparation.Grid.op_prefix_cumulative line 255
  12. lemma OAI.CPTSeparation.Operational.Machine.cumulativeAccepts_fintype line 281
  13. theorem OAI.CPTSeparation.Grid.cumulative_cutoff_agrees_on_some_box line 296
  14. theorem OAI.CPTSeparation.query_not_cumulative_cutoff_HF line 363
  15. def OAI.CPTSeparation.Operational.Machine.polynomialCumulativeAccepts line 375
  16. theorem OAI.CPTSeparation.Grid.polynomial_cumulative_agrees_on_some_box line 387
  17. theorem OAI.CPTSeparation.query_not_polynomial_cumulative_HF line 468