OAI/Combinatorics/RamseyFive/Geometry/TwoFinitePublic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpRamseyFive.ScoreGeometry.TwoPublicTape line 16
2. abbrev OAI.SharpRamseyFive.ScoreGeometry.TwoPublicMessage line 18
3. def OAI.SharpRamseyFive.ScoreGeometry.twoPublicLaw line 21
4. def OAI.SharpRamseyFive.ScoreGeometry.twoPublicDecoded line 25
5. def OAI.SharpRamseyFive.ScoreGeometry.twoPublicEncoded line 30
6. theorem OAI.SharpRamseyFive.ScoreGeometry.twoPublic_output_law line 37
7. theorem OAI.SharpRamseyFive.ScoreGeometry.twoPublic_oriented line 56