OAI/Computability/WLIdentification/RefinementCorrectness.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLIdentification.NumericWL.pair_bound line 10
  2. theorem OAI.WLIdentification.NumericWL.pairTable_lookup line 15
  3. theorem OAI.WLIdentification.NumericWL.transTable_lookup line 20
  4. abbrev OAI.WLIdentification.NumericWL.sides line 29
  5. theorem OAI.WLIdentification.NumericWL.sides_inl line 31
  6. theorem OAI.WLIdentification.NumericWL.sides_inr line 32
  7. theorem OAI.WLIdentification.NumericWL.left_inl line 33
  8. theorem OAI.WLIdentification.NumericWL.left_inr line 35
  9. theorem OAI.WLIdentification.NumericWL.code_inl line 37
  10. theorem OAI.WLIdentification.NumericWL.code_inr line 39
  11. theorem OAI.WLIdentification.NumericWL.equalCounts_correct line 42
  12. def OAI.WLIdentification.NumericWL.neighborData line 72
  13. theorem OAI.WLIdentification.NumericWL.neighborEncoded line 76
  14. def OAI.WLIdentification.NumericWL.nc line 93
  15. theorem OAI.WLIdentification.NumericWL.neighbor_vectors line 97
  16. theorem OAI.WLIdentification.NumericWL.neighbor_correct line 109
  17. abbrev OAI.WLIdentification.NumericWL.tuples line 144
  18. def OAI.WLIdentification.NumericWL.te line 146
  19. theorem OAI.WLIdentification.NumericWL.te_inl line 149
  20. theorem OAI.WLIdentification.NumericWL.te_inr line 151
  21. theorem OAI.WLIdentification.NumericWL.te_symm_inl line 154
  22. theorem OAI.WLIdentification.NumericWL.te_symm_inr line 160
  23. theorem OAI.WLIdentification.NumericWL.digit_function line 167
  24. def OAI.WLIdentification.NumericWL.tupleData line 171
  25. theorem OAI.WLIdentification.NumericWL.digits_update line 177
  26. theorem OAI.WLIdentification.NumericWL.tupleEncoded line 200
  27. def OAI.WLIdentification.NumericWL.tc line 230
  28. theorem OAI.WLIdentification.NumericWL.tuple_vectors line 234
  29. theorem OAI.WLIdentification.NumericWL.forall_bound2 line 243
  30. theorem OAI.WLIdentification.NumericWL.tupleInitial_correct line 247
  31. theorem OAI.WLIdentification.NumericWL.tuple_correct line 262
  32. theorem OAI.WLIdentification.WordExpressions.Poly.eqtest line 303