OAI/Combinatorics/RamseyFive/Geometry/FourFinitePredictor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.ScoreGeometry.fourFinitePredictor line 13
  2. theorem OAI.SharpRamseyFive.ScoreGeometry.eventually_four_finite_predictor line 31
  3. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.FiniteNodeTape line 110
  4. def OAI.SharpRamseyFive.ProjectiveIncidence.finiteNodeTapeLaw line 112
  5. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.FiniteNodeMessage line 115
  6. def OAI.SharpRamseyFive.ProjectiveIncidence.finiteNodeDecoded line 118
  7. def OAI.SharpRamseyFive.ProjectiveIncidence.finiteNodeEncoded line 122
  8. def OAI.SharpRamseyFive.ProjectiveIncidence.finiteNodeCost line 130
  9. def OAI.SharpRamseyFive.ProjectiveIncidence.finiteNodeNextOut line 134
  10. def OAI.SharpRamseyFive.ProjectiveIncidence.finiteNodeNextLaw line 141
  11. def OAI.SharpRamseyFive.ProjectiveIncidence.finiteNodeOutput line 145
  12. lemma OAI.SharpRamseyFive.ProjectiveIncidence.finiteNode_exact line 153
  13. lemma OAI.SharpRamseyFive.ProjectiveIncidence.finiteNode_law line 165
  14. lemma OAI.SharpRamseyFive.ProjectiveIncidence.finiteNode_prefixes line 179