OAI/NumberTheory/Ostmann/Construction/CanonicalOccurrenceTransportCode.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Ostmann.Construction.CanonicalOccurrenceTransport.StateCode line 11
  2. theorem OAI.Ostmann.Construction.CanonicalOccurrenceTransport.StateCode.ext line 16
  3. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.stateCode line 22
  4. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.TreeCode line 25
  5. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.treeCode line 29
  6. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.select line 34
  7. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.permutationOrder line 37
  8. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.select_ofFn line 40
  9. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.reorder_code line 48
  10. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.leftPart_code line 53
  11. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.rightPart_code line 62
  12. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.append_code line 71
  13. inductive OAI.Ostmann.Construction.CanonicalOccurrenceTransport.Plan line 96
  14. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.plan line 101
  15. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.CompensationCode line 111
  16. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.compensationCode line 115
  17. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.execute line 123
  18. theorem OAI.Ostmann.Construction.CanonicalOccurrenceTransport.encode_code line 134