OAI/Combinatorics/VariableWL/Decision.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Encoding.entry line 8
  2. def OAI.VariableWL.Encoding.MatrixValid line 10
  3. def OAI.VariableWL.Encoding.fromMatrix line 14
  4. theorem OAI.VariableWL.Encoding.entry_matrix line 21
  5. theorem OAI.VariableWL.Encoding.matrix_valid line 38
  6. theorem OAI.VariableWL.Encoding.fromMatrix_matrix line 47
  7. theorem OAI.VariableWL.Encoding.matrix_fromMatrix line 57
  8. def OAI.VariableWL.Encoding.readMatrix line 72
  9. theorem OAI.VariableWL.Encoding.readMatrix_matrix line 75
  10. theorem OAI.VariableWL.Encoding.readMatrix_sound line 78
  11. def OAI.VariableWL.Encoding.graph line 85
  12. theorem OAI.VariableWL.Encoding.graph_code line 90
  13. theorem OAI.VariableWL.Encoding.graph_sound line 98
  14. def OAI.VariableWL.Encoding.pair line 110
  15. theorem OAI.VariableWL.Encoding.pair_code line 119
  16. theorem OAI.VariableWL.Encoding.pair_sound line 128
  17. theorem OAI.VariableWL.Encoding.pair_eq_some_iff line 152
  18. theorem OAI.VariableWL.Encoding.malformed_not_WL line 155
  19. theorem OAI.VariableWL.Encoding.malformed_not_SubWL line 160
  20. def OAI.VariableWL.RefinementArray.count line 171
  21. def OAI.VariableWL.RefinementArray.numbering line 173
  22. def OAI.VariableWL.RefinementArray.pack line 176
  23. def OAI.VariableWL.RefinementArray.lookup line 180
  24. theorem OAI.VariableWL.RefinementArray.lookup_pack line 183
  25. theorem OAI.VariableWL.RefinementArray.pack_length line 202
  26. def OAI.VariableWL.RefinementArray.array line 205
  27. theorem OAI.VariableWL.RefinementArray.array_length line 209
  28. theorem OAI.VariableWL.RefinementArray.array_correct line 212
  29. def OAI.VariableWL.RefinementArray.accepts line 222
  30. theorem OAI.VariableWL.RefinementArray.accepts_correct line 225
  31. def OAI.VariableWL.InputDecision.capped line 235
  32. theorem OAI.VariableWL.InputDecision.capped_pos line 237
  33. theorem OAI.VariableWL.InputDecision.equivalent_capped line 241
  34. def OAI.VariableWL.InputDecision.general line 251
  35. theorem OAI.VariableWL.InputDecision.general_correct line 256
  36. def OAI.VariableWL.PromiseDecision.reach line 272
  37. theorem OAI.VariableWL.PromiseDecision.reach_correct line 277
  38. theorem OAI.VariableWL.PromiseDecision.reach_order line 300
  39. def OAI.VariableWL.PromiseDecision.connected line 308
  40. theorem OAI.VariableWL.PromiseDecision.connected_correct line 311
  41. def OAI.VariableWL.PromiseDecision.neighbors line 321
  42. theorem OAI.VariableWL.PromiseDecision.neighbors_length line 324
  43. def OAI.VariableWL.PromiseDecision.subcubic line 333
  44. theorem OAI.VariableWL.PromiseDecision.subcubic_correct line 335
  45. def OAI.VariableWL.InputDecision.subcubic line 343
  46. theorem OAI.VariableWL.InputDecision.subcubic_correct line 351