OAI/SetTheory/PartitionPrinciple/Geometry/GroundFiniteWordLaws.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.natSuccessorEntryFormula line 15
  2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_natSuccessorEntryFormula line 19
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.natAddEntryFormula line 26
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_natAddEntryFormula line 35
  5. def OAI.PartitionPilot.Forcing.BoundedFormula.natMulEntryFormula line 66
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_natMulEntryFormula line 76
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.natSuccessorGraph_mem line 137
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.naturalFiniteTrace_mem_relations line 168
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.natAddGraph_mem line 183
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.natMulGraph_mem line 236
  11. def OAI.PartitionPilot.Forcing.BoundedFormula.finiteWordMapEntryFormula line 305
  12. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_finiteWordMapEntryFormula line 309
  13. def OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordMapGraph line 323
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_finiteWordMapGraph line 328
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordMapGraph_mem line 340
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordMapGraph_eq_graph line 373
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordMapGraph_function line 398
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.finiteWordAppendEntryFormula line 413
  19. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_finiteWordAppendEntryFormula line 419
  20. def OAI.PartitionPilot.Forcing.BoundedFormula.finiteWordReverseEntryFormula line 429
  21. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_finiteWordReverseEntryFormula line 434
  22. def OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordAppendGraph line 448
  23. def OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordReverseGraph line 454
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_finiteWordAppendGraph line 459
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_finiteWordReverseGraph line 473
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordAppendGraph_mem line 485
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordReverseGraph_mem line 510
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordAppendGraph_eq_graph line 538
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordReverseGraph_eq_graph line 569
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordAppendGraph_function line 594
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordReverseGraph_function line 606
  32. def OAI.PartitionPilot.Forcing.externalWordInverse line 622
  33. theorem OAI.PartitionPilot.Forcing.externalWordInverse_involutive line 625
  34. theorem OAI.PartitionPilot.Forcing.externalWordInverse_append line 635
  35. theorem OAI.PartitionPilot.Forcing.compose_presentation_graphs line 640
  36. def OAI.PartitionPilot.Forcing.TransitiveGround.externalInverseWordGraph line 667
  37. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalInverseWordGraph_mem line 674
  38. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalInverseWordGraph_eq_graph line 695
  39. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalInverseWordGraph_entry_iff line 721
  40. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalInverseWordGraph_function line 731
  41. theorem OAI.PartitionPilot.Forcing.TransitiveGround.decodeWord line 750
  42. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordAppend_empty line 756
  43. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordAppend_assoc line 776
  44. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordReverse_involution line 798
  45. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordReverse_append line 811
  46. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordLength_append line 836
  47. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordLength_reverse line 857