OAI/ModelTheory/Choiceless/Traces.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CPTSeparation.Hereditary.descendants line 15
  2. lemma OAI.CPTSeparation.Hereditary.descendants_mono line 19
  3. lemma OAI.CPTSeparation.Hereditary.roots_subset_descendants line 21
  4. lemma OAI.CPTSeparation.Hereditary.descendants_subset line 26
  5. lemma OAI.CPTSeparation.Hereditary.descendants_stable line 36
  6. lemma OAI.CPTSeparation.Hereditary.descendants_card_lower line 53
  7. lemma OAI.CPTSeparation.Hereditary.descendants_eq line 70
  8. lemma OAI.CPTSeparation.Operational.State.mem_critical_iff line 105
  9. lemma OAI.CPTSeparation.Operational.State.uniform_critical line 124
  10. def OAI.CPTSeparation.Operational.State.rootFamily line 187
  11. lemma OAI.CPTSeparation.Operational.State.uniform_roots line 191
  12. lemma OAI.CPTSeparation.Operational.State.uniform_descendants line 213
  13. lemma OAI.CPTSeparation.Operational.State.uniform_active line 242
  14. lemma OAI.CPTSeparation.Operational.State.uniform_active_card line 255
  15. lemma OAI.CPTSeparation.Operational.uniform_consistency line 288
  16. lemma OAI.CPTSeparation.Grid.op_observations_agree line 342
  17. lemma OAI.CPTSeparation.Operational.State.active_apply_subset line 434
  18. lemma OAI.CPTSeparation.Operational.State.initial_active_card line 469
  19. def OAI.CPTSeparation.Operational.Machine.boundedAccepts line 510
  20. lemma OAI.CPTSeparation.Operational.Machine.step_exists_iff line 514
  21. lemma OAI.CPTSeparation.Operational.Machine.active_step_bound line 522
  22. def OAI.CPTSeparation.Operational.Machine.PrefixBound line 555
  23. def OAI.CPTSeparation.Operational.Machine.ObservationsAt line 558
  24. lemma OAI.CPTSeparation.Operational.Machine.bounded_accept_transfer line 565
  25. lemma OAI.CPTSeparation.Operational.Machine.bounded_accept_iff line 652
  26. lemma OAI.CPTSeparation.Grid.op_prefix_observations line 670
  27. lemma OAI.CPTSeparation.PolynomialCost.eval_mono line 704
  28. def OAI.CPTSeparation.Operational.Machine.cutoffAccepts line 713
  29. lemma OAI.CPTSeparation.Grid.atom_card_independent line 727
  30. lemma OAI.CPTSeparation.Operational.Machine.boundedAccepts_fintype line 747
  31. theorem OAI.CPTSeparation.Grid.cutoff_agrees_on_some_box line 762