OAI/Computability/WLIdentification/NumericRefinement.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLIdentification.NumericWL.left line 10
  2. def OAI.WLIdentification.NumericWL.code line 11
  3. def OAI.WLIdentification.NumericWL.pairTable line 13
  4. def OAI.WLIdentification.NumericWL.transTable line 16
  5. def OAI.WLIdentification.NumericWL.equalCounts line 20
  6. def OAI.WLIdentification.NumericWL.selectedEdge line 25
  7. def OAI.WLIdentification.NumericWL.neighborActive line 28
  8. def OAI.WLIdentification.NumericWL.neighborTrans line 31
  9. def OAI.WLIdentification.NumericWL.neighbor line 34
  10. def OAI.WLIdentification.NumericWL.tupleInitial line 39
  11. def OAI.WLIdentification.NumericWL.tupleTrans line 46
  12. def OAI.WLIdentification.NumericWL.tuple line 50
  13. def OAI.WLIdentification.NumericWL.equivalent line 56
  14. theorem OAI.WLIdentification.NumericWL.left_poly line 64
  15. theorem OAI.WLIdentification.NumericWL.code_poly line 67
  16. theorem OAI.WLIdentification.NumericWL.selectedEdge_poly line 70
  17. theorem OAI.WLIdentification.NumericWL.equalCounts_poly line 76
  18. theorem OAI.WLIdentification.NumericWL.neighborActive_poly line 94
  19. theorem OAI.WLIdentification.NumericWL.neighborTrans_poly line 99
  20. theorem OAI.WLIdentification.NumericWL.tupleInitial_poly line 108
  21. theorem OAI.WLIdentification.NumericWL.tupleTrans_poly line 119
  22. theorem OAI.WLIdentification.NumericKernel.table_poly_of line 143
  23. theorem OAI.WLIdentification.NumericWL.equalCounts_poly_of line 154
  24. theorem OAI.WLIdentification.NumericWL.neighborActive_poly_of line 165
  25. theorem OAI.WLIdentification.NumericWL.neighborTrans_poly_of line 176
  26. theorem OAI.WLIdentification.NumericWL.tupleInitial_poly_of line 187
  27. theorem OAI.WLIdentification.NumericWL.tupleTrans_poly_of line 198
  28. theorem OAI.WLIdentification.NumericGraph.simple_poly_of line 210
  29. theorem OAI.WLIdentification.NumericGraph.iso_poly_of line 221
  30. theorem OAI.WLIdentification.NumericGraph.mate_poly_of line 232
  31. theorem OAI.WLIdentification.NumericWL.neighborActiveTable_poly line 244
  32. theorem OAI.WLIdentification.NumericWL.neighborTransTable_poly line 251
  33. theorem OAI.WLIdentification.NumericWL.trueTable_poly line 260
  34. theorem OAI.WLIdentification.NumericWL.tupleInitialTable_poly line 265
  35. theorem OAI.WLIdentification.NumericWL.tupleTransTable_poly line 273
  36. theorem OAI.WLIdentification.NumericWL.neighborActiveTable_poly_of line 288
  37. theorem OAI.WLIdentification.NumericWL.neighborTransTable_poly_of line 295
  38. theorem OAI.WLIdentification.NumericWL.tupleInitialTable_poly_of line 301
  39. theorem OAI.WLIdentification.NumericWL.tupleTransTable_poly_of line 308
  40. theorem OAI.WLIdentification.NumericWL.neighbor_poly_of line 315
  41. theorem OAI.WLIdentification.NumericWL.tuple_poly_of line 322
  42. theorem OAI.WLIdentification.NumericWL.equivalent_poly_of line 330