OAI/SetTheory/PartitionPrinciple/Definability/ExternalWordRewriteRelations.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.Factor line 15
  2. instance OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.factorGroup line 19
  3. abbrev OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.External line 22
  4. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.old line 24
  5. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.free line 25
  6. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.generator line 26
  7. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.signed line 27
  8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.old_injective line 29
  9. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.Cancel line 31
  10. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.Reduced line 33
  11. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.eval line 38
  12. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.oldWord line 44
  13. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.oldWord_prod line 48
  14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.oldWord_not_free line 57
  15. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.free_head_not_old line 65
  16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.free_prepend line 76
  17. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.signed_mul_free line 90
  18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.head_nontrivial line 99
  19. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.relative_normal_form line 104
  20. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.reduced_not_old line 139
  21. abbrev OAI.PartitionPilot.Forcing.ExternalWordRewrite.Alphabet line 158
  22. inductive OAI.PartitionPilot.Forcing.ExternalWordRewrite.Atomic line 162
  23. def OAI.PartitionPilot.Forcing.ExternalWordRewrite.Step line 167
  24. def OAI.PartitionPilot.Forcing.ExternalWordRewrite.Path line 172
  25. def OAI.PartitionPilot.Forcing.ExternalWordRewrite.congruence line 175
  26. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.Atomic.step line 178
  27. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.Step.symm line 181
  28. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.Step.append_left line 185
  29. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.Step.append_right line 193
  30. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.Path.symm line 201
  31. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.Path.append line 206
  32. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.Step.to_congruence line 211
  33. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.path_iff_conGen line 222