OAI/Combinatorics/RamseyFive/Geometry/GeneralReversedCode.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpRamseyFive.ScoreGeometry.GeneralReversedTape line 14
2. abbrev OAI.SharpRamseyFive.ScoreGeometry.GeneralReversedMessage line 17
3. def OAI.SharpRamseyFive.ScoreGeometry.generalReversedDecoded line 20
4. def OAI.SharpRamseyFive.ScoreGeometry.generalReversedEncoded line 24
5. def OAI.SharpRamseyFive.ScoreGeometry.generalReversedCost line 31
6. lemma OAI.SharpRamseyFive.ScoreGeometry.generalReversed_exact line 37
7. theorem OAI.SharpRamseyFive.ScoreGeometry.generalReversed_law line 53
8. lemma OAI.SharpRamseyFive.ScoreGeometry.generalReversed_prefixes line 70
9. theorem OAI.SharpRamseyFive.ScoreGeometry.generalReversed_cost line 90
10. structure OAI.SharpRamseyFive.ScoreGeometry.FinitePredictor line 122
11. def OAI.SharpRamseyFive.ScoreGeometry.FinitePredictor.output line 133
12. instance OAI.SharpRamseyFive.ScoreGeometry.(instance at line 141) line 141
13. def OAI.SharpRamseyFive.ScoreGeometry.threeFinitePredictor line 153