OAI/SetTheory/PartitionPrinciple/Geometry/TileStarIncomingCodes.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.FiniteRelationPathCode line 13
  2. theorem OAI.PartitionPilot.Forcing.IterationTraceCode.reflTransGen line 17
  3. theorem OAI.PartitionPilot.Forcing.FiniteRelationPathCode.reflTransGen line 46
  4. theorem OAI.PartitionPilot.Forcing.finiteWordGraph_chain_trace line 57
  5. theorem OAI.PartitionPilot.Forcing.finiteWordGraph_chain_path line 76
  6. theorem OAI.PartitionPilot.Forcing.reflTransGen_iff_finiteWordGraph_path line 89
  7. inductive OAI.PartitionPilot.Forcing.RelationPathSteps line 106
  8. theorem OAI.PartitionPilot.Forcing.chain_append_last line 110
  9. theorem OAI.PartitionPilot.Forcing.RelationPathSteps.append line 122
  10. theorem OAI.PartitionPilot.Forcing.RelationPathSteps.cons line 128
  11. theorem OAI.PartitionPilot.Forcing.RelationPathSteps.chain line 131
  12. theorem OAI.PartitionPilot.Forcing.IterationTraceCode.pathSteps line 144
  13. theorem OAI.PartitionPilot.Forcing.RelationPathSteps.exists_trace line 168
  14. def OAI.PartitionPilot.Forcing.BoundedFormula.finiteRelationPathFormula line 191
  15. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_finiteRelationPathFormula line 196
  16. def OAI.PartitionPilot.Forcing.BoundedFormula.finitePathClosureEntryFormula line 213
  17. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_finitePathClosureEntryFormula line 219
  18. def OAI.PartitionPilot.Forcing.TransitiveGround.finitePathClosure line 246
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_finitePathClosure_iff line 250
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finitePathClosure_subset line 261
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finitePathClosure_mem line 265
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_finitePathClosure line 292
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finitePathClosure_equivalence line 330
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finitePathQuotient_spec line 352
  25. def OAI.PartitionPilot.Forcing.TransitiveGround.relationPathLengths line 378
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_relationPathLengths line 383
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationPathLengths_subset line 395
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationPathLengths_mem line 398
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationPathLengths_iff_steps line 420
  30. def OAI.PartitionPilot.Forcing.shortestLengthGraph line 448
  31. theorem OAI.PartitionPilot.Forcing.pair_mem_shortestLengthGraph line 452
  32. def OAI.PartitionPilot.Forcing.BoundedFormula.shortestLengthEntryFormula line 464
  33. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_shortestLengthEntryFormula line 469
  34. theorem OAI.PartitionPilot.Forcing.TransitiveGround.shortestLengthGraph_mem line 479
  35. def OAI.PartitionPilot.Forcing.TransitiveGround.relationDepthGraph line 499
  36. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationDepthGraph_mem line 502
  37. theorem OAI.PartitionPilot.Forcing.shortestLengthGraph_entry line 518
  38. theorem OAI.PartitionPilot.Forcing.shortestLengthGraph_eq_graph line 532
  39. def OAI.PartitionPilot.Forcing.LowerDepthEdgeCode line 555
  40. def OAI.PartitionPilot.Forcing.treeParentGraph line 559
  41. theorem OAI.PartitionPilot.Forcing.pair_mem_treeParentGraph line 563
  42. def OAI.PartitionPilot.Forcing.BoundedFormula.lowerDepthEdgeFormula line 575
  43. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_lowerDepthEdgeFormula line 580
  44. def OAI.PartitionPilot.Forcing.BoundedFormula.treeParentEntryFormula line 586
  45. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_treeParentEntryFormula line 591
  46. theorem OAI.PartitionPilot.Forcing.TransitiveGround.treeParentGraph_mem line 601
  47. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.Follows.pathSteps line 633
  48. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.follows_of_pathSteps line 639
  49. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.depth_pathSteps line 652
  50. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.depth_le_steps line 656
  51. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.depthGraph_eq_graph line 672
  52. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.depthGraph_spec line 690
  53. def OAI.PartitionPilot.Forcing.treeNonrootCarrier line 713
  54. def OAI.PartitionPilot.Forcing.treeIncomingGraph line 716
  55. theorem OAI.PartitionPilot.Forcing.pair_mem_treeIncomingGraph line 721
  56. def OAI.PartitionPilot.Forcing.BoundedFormula.treeIncomingEntryFormula line 734
  57. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_treeIncomingEntryFormula line 741
  58. theorem OAI.PartitionPilot.Forcing.TransitiveGround.treeNonrootCarrier_mem line 752
  59. theorem OAI.PartitionPilot.Forcing.TransitiveGround.treeIncomingGraph_mem line 758
  60. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.incomingGraph_entry line 793
  61. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.incomingGraph_function line 813
  62. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.TileStars.incomingGraph_spec line 832