OAI/Computability/WitnessedChoice/TraceGraphs.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WitnessedSeparation.Operational.Rule.Graph line 16
  2. lemma OAI.WitnessedSeparation.Operational.Rule.graph_sound line 32
  3. lemma OAI.WitnessedSeparation.Operational.Rule.graph_complete line 71
  4. def OAI.WitnessedSeparation.Operational.Rule.width line 141
  5. lemma OAI.WitnessedSeparation.Operational.Rule.uniform_graph line 170
  6. def OAI.WitnessedSeparation.Operational.Closed line 243
  7. lemma OAI.WitnessedSeparation.Operational.Closed.closure line 248
  8. lemma OAI.WitnessedSeparation.Operational.Closed.union line 251
  9. lemma OAI.WitnessedSeparation.Operational.Closed.biUnion line 258
  10. lemma OAI.WitnessedSeparation.Operational.Closed.insert line 264
  11. lemma OAI.WitnessedSeparation.Operational.Term.trace_closed line 274
  12. lemma OAI.WitnessedSeparation.Operational.Rule.trace_closed line 294
  13. lemma OAI.WitnessedSeparation.Operational.State.value_apply_iff line 322
  14. lemma OAI.WitnessedSeparation.Operational.uniform_updates line 367
  15. lemma OAI.WitnessedSeparation.Operational.uniform_applyUpdates line 388
  16. lemma OAI.WitnessedSeparation.Operational.lift_closure line 420
  17. lemma OAI.WitnessedSeparation.Operational.lift_cons line 423
  18. lemma OAI.WitnessedSeparation.Operational.Term.trace_transport line 429
  19. lemma OAI.WitnessedSeparation.Operational.Rule.trace_transport line 467
  20. lemma OAI.WitnessedSeparation.Operational.Machine.uniform_flag line 527
  21. lemma OAI.WitnessedSeparation.Operational.Machine.uniform_step line 548
  22. def OAI.WitnessedSeparation.Operational.Machine.runTrace line 596
  23. lemma OAI.WitnessedSeparation.Operational.Machine.rule_trace_subset line 601
  24. lemma OAI.WitnessedSeparation.Operational.Machine.active_subset_trace line 607
  25. lemma OAI.WitnessedSeparation.Operational.Machine.runTrace_closed line 611
  26. lemma OAI.WitnessedSeparation.Operational.Machine.card_runTrace_le line 619
  27. lemma OAI.WitnessedSeparation.Operational.Machine.runTrace_transport line 639
  28. lemma OAI.WitnessedSeparation.Operational.Machine.uniform_run line 685
  29. lemma OAI.WitnessedSeparation.Operational.Machine.uniform_run_flag line 714
  30. lemma OAI.WitnessedSeparation.Grid.opTrace_supported line 739
  31. lemma OAI.WitnessedSeparation.Grid.program_atom_mem line 760
  32. lemma OAI.WitnessedSeparation.Grid.op_input_uniform line 771
  33. lemma OAI.WitnessedSeparation.Grid.op_flag_agrees line 793
  34. lemma OAI.WitnessedSeparation.PolynomialCost.eval_bound line 847
  35. lemma OAI.WitnessedSeparation.Operational.Machine.run_none line 881
  36. lemma OAI.WitnessedSeparation.Operational.Machine.run_prefix_exists line 893
  37. lemma OAI.WitnessedSeparation.Operational.Machine.halted_persists line 899
  38. lemma OAI.WitnessedSeparation.Operational.Machine.run_total_of_halts line 912
  39. lemma OAI.WitnessedSeparation.Operational.Machine.active_card_of_halts line 919
  40. lemma OAI.WitnessedSeparation.Operational.Machine.flag_accept_eq_of_halts line 929
  41. lemma OAI.WitnessedSeparation.Operational.Machine.exists_palette line 958
  42. theorem OAI.WitnessedSeparation.Grid.operational_agrees_on_some_box line 980
  43. theorem OAI.WitnessedSeparation.query_not_intrinsically_bounded_HF line 1042
  44. def OAI.WitnessedSeparation.Hereditary.descendants line 1065
  45. lemma OAI.WitnessedSeparation.Hereditary.descendants_mono line 1069
  46. lemma OAI.WitnessedSeparation.Hereditary.roots_subset_descendants line 1071
  47. lemma OAI.WitnessedSeparation.Hereditary.descendants_subset line 1076
  48. lemma OAI.WitnessedSeparation.Hereditary.descendants_stable line 1086
  49. lemma OAI.WitnessedSeparation.Hereditary.descendants_card_lower line 1103
  50. lemma OAI.WitnessedSeparation.Hereditary.descendants_eq line 1120