OAI/Computability/WitnessedChoice/ChoiceSeparation.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.fundamentalPool_in_cycleSet line 20
  2. lemma OAI.WitnessedChoice.RelationPools.witnessPool_mono line 86
  3. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.selection_transitive line 116
  4. abbrev OAI.WitnessedSeparation.Grid.ConfigAtom line 150
  5. def OAI.WitnessedSeparation.Grid.configBlock line 152
  6. lemma OAI.WitnessedSeparation.Grid.mem_configBlock line 155
  7. def OAI.WitnessedSeparation.Grid.atEdge line 167
  8. def OAI.WitnessedSeparation.Grid.ParentEdges.allowedConfig line 173
  9. def OAI.WitnessedSeparation.Grid.ParentEdges.configCompatibility line 176
  10. def OAI.WitnessedSeparation.Grid.ParentEdges.testProblem line 180
  11. lemma OAI.WitnessedSeparation.Grid.ParentEdges.solution_configs line 190
  12. lemma OAI.WitnessedSeparation.Grid.ParentEdges.exists_globals_of_solution line 210
  13. lemma OAI.WitnessedSeparation.Grid.ParentEdges.test_solution_of_zero line 232
  14. lemma OAI.WitnessedSeparation.Grid.ParentEdges.zero_of_test_solution line 250
  15. theorem OAI.WitnessedSeparation.Grid.ParentEdges.test_iff_zero line 256
  16. lemma OAI.WitnessedSeparation.Grid.atom_mem_state line 278
  17. lemma OAI.WitnessedSeparation.Grid.chosen_incident_iff line 281
  18. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_edgeDiff line 306
  19. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_allowed line 321
  20. lemma OAI.WitnessedSeparation.Grid.common_edge_unique line 355
  21. lemma OAI.WitnessedSeparation.Grid.atom_config_mem line 366
  22. lemma OAI.WitnessedSeparation.Grid.ParentEdges.compatible_edge_iff line 375
  23. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_support line 393
  24. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_unsupported line 412
  25. lemma OAI.WitnessedSeparation.Grid.configAtoms_grid line 469
  26. lemma OAI.WitnessedSeparation.Grid.config_mem_vertexCode line 480
  27. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_deletedStep line 498
  28. lemma OAI.WitnessedChoice.TreeTest.Problem.run_eq_finite line 566
  29. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.value_deletion line 587
  30. lemma OAI.WitnessedSeparation.Grid.selected_inter_singleton line 646
  31. lemma OAI.WitnessedSeparation.Grid.edgeState_subset_edgeAtoms line 660
  32. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_complete line 671
  33. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_survives line 702
  34. lemma OAI.WitnessedSeparation.Grid.testProblem_block line 744
  35. lemma OAI.WitnessedSeparation.Grid.survivors_test_iff_zero line 748
  36. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.value_output line 767
  37. lemma OAI.WitnessedChoice.BGS.Realizes.first_encode line 839
  38. lemma OAI.WitnessedChoice.BGS.Realizes.value_constant line 854
  39. lemma OAI.WitnessedChoice.BGS.GuardedProgram.value_constant line 885
  40. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.terminal_output line 922
  41. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.body_value line 937
  42. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.mem_grid_blockParameters line 969
  43. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.mem_parameters line 983
  44. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.mem_parameterTerm line 1004
  45. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.parameterTerm_nonempty line 1019
  46. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.formula_value line 1047