OAI/ModelTheory/Choiceless/Simulation.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CPTSeparation.Operational.Closed line 17
  2. lemma OAI.CPTSeparation.Operational.Closed.closure line 22
  3. lemma OAI.CPTSeparation.Operational.Closed.union line 27
  4. lemma OAI.CPTSeparation.Operational.Closed.biUnion line 36
  5. lemma OAI.CPTSeparation.Operational.Closed.insert line 44
  6. lemma OAI.CPTSeparation.Operational.Term.trace_closed line 56
  7. lemma OAI.CPTSeparation.Operational.Rule.trace_closed line 76
  8. lemma OAI.CPTSeparation.Operational.State.value_apply_iff line 100
  9. lemma OAI.CPTSeparation.Operational.uniform_updates line 145
  10. lemma OAI.CPTSeparation.Operational.uniform_applyUpdates line 165
  11. lemma OAI.CPTSeparation.Operational.lift_closure line 203
  12. lemma OAI.CPTSeparation.Operational.lift_cons line 210
  13. lemma OAI.CPTSeparation.Operational.Term.trace_transport line 220
  14. lemma OAI.CPTSeparation.Operational.Rule.trace_transport line 258
  15. lemma OAI.CPTSeparation.Operational.Machine.uniform_flag line 313
  16. lemma OAI.CPTSeparation.Operational.Machine.uniform_step line 351
  17. def OAI.CPTSeparation.Operational.Machine.runTrace line 395
  18. lemma OAI.CPTSeparation.Operational.Machine.rule_trace_subset line 400
  19. lemma OAI.CPTSeparation.Operational.Machine.active_subset_trace line 406
  20. lemma OAI.CPTSeparation.Operational.Machine.runTrace_closed line 410
  21. lemma OAI.CPTSeparation.Operational.Machine.card_runTrace_le line 418
  22. lemma OAI.CPTSeparation.Operational.Machine.runTrace_transport line 438
  23. lemma OAI.CPTSeparation.Operational.Machine.uniform_run line 478
  24. lemma OAI.CPTSeparation.Operational.Machine.uniform_run_flag line 507
  25. lemma OAI.CPTSeparation.Grid.opTrace_supported line 528
  26. lemma OAI.CPTSeparation.Grid.program_atom_mem line 549
  27. lemma OAI.CPTSeparation.Grid.op_input_uniform line 560
  28. lemma OAI.CPTSeparation.Grid.op_flag_agrees line 576
  29. lemma OAI.CPTSeparation.PolynomialCost.eval_bound line 626
  30. lemma OAI.CPTSeparation.Operational.Machine.run_none line 658
  31. lemma OAI.CPTSeparation.Operational.Machine.run_prefix_exists line 670
  32. lemma OAI.CPTSeparation.Operational.Machine.halted_persists line 676
  33. lemma OAI.CPTSeparation.Operational.Machine.run_total_of_halts line 689
  34. lemma OAI.CPTSeparation.Operational.Machine.active_card_of_halts line 696
  35. lemma OAI.CPTSeparation.Operational.Machine.flag_accept_eq_of_halts line 706
  36. lemma OAI.CPTSeparation.Operational.Machine.exists_palette line 729
  37. theorem OAI.CPTSeparation.Grid.operational_agrees_on_some_box line 745
  38. theorem OAI.CPTSeparation.query_not_intrinsically_bounded_HF line 803