OAI/Combinatorics/VariableWL/PrefixDescriptor.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.PrefixDescriptor.raw_injective line 13
  2. theorem OAI.VariableWL.PrefixDescriptor.raw_surjective line 45
  3. def OAI.VariableWL.PrefixDescriptor.presentation line 88
  4. theorem OAI.VariableWL.PrefixDescriptor.presentation_encode line 111
  5. def OAI.VariableWL.PrefixAlphabet.trim line 118
  6. theorem OAI.VariableWL.PrefixAlphabet.trim_encode line 120
  7. def OAI.VariableWL.PrefixDescriptor.Data.forward line 133
  8. def OAI.VariableWL.PrefixDescriptor.Data.slot line 140
  9. def OAI.VariableWL.PrefixDescriptor.Data.internal line 146
  10. theorem OAI.VariableWL.PrefixDescriptor.raw_forward line 154
  11. theorem OAI.VariableWL.PrefixDescriptor.fin_val_ite line 166
  12. theorem OAI.VariableWL.PrefixDescriptor.fin_val_dite line 168
  13. theorem OAI.VariableWL.PrefixDescriptor.raw_slot line 170
  14. theorem OAI.VariableWL.PrefixDescriptor.raw_internal line 183
  15. def OAI.VariableWL.PrefixDescriptor.sortRaw line 207
  16. theorem OAI.VariableWL.PrefixDescriptor.sortRaw_block line 212
  17. theorem OAI.VariableWL.PrefixDescriptor.sortRaw_injective line 215
  18. theorem OAI.VariableWL.PrefixDescriptor.sortRaw_bounds line 248
  19. theorem OAI.VariableWL.PrefixDescriptor.sortRaw_valid line 262
  20. def OAI.VariableWL.PrefixDescriptor.Data.sortPredicate line 275
  21. def OAI.VariableWL.PrefixDescriptor.Data.color line 276
  22. def OAI.VariableWL.PrefixDescriptor.Data.colorBound line 277
  23. theorem OAI.VariableWL.PrefixDescriptor.sortPresentation line 280
  24. def OAI.VariableWL.Computation.Stack.PolyRecipe.table₂ line 343
  25. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.table₂_number line 345
  26. def OAI.VariableWL.Computation.Stack.PolyRecipe.table₃ line 352
  27. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.table₃_number line 355
  28. theorem OAI.VariableWL.PrefixAlphabet.truncate_cap line 367
  29. theorem OAI.VariableWL.PrefixAlphabet.prefixCode_cap line 373
  30. theorem OAI.VariableWL.PrefixAlphabet.trim_cap line 380
  31. theorem OAI.VariableWL.PrefixAlphabet.prefixCode_zero line 387
  32. theorem OAI.VariableWL.PrefixAlphabet.trim_zero line 392
  33. theorem OAI.VariableWL.PrefixAlphabet.bit_zero line 393
  34. def OAI.VariableWL.PrefixAlphabet.TotalProgram.prefixCode line 405
  35. def OAI.VariableWL.PrefixAlphabet.TotalProgram.trim line 407
  36. def OAI.VariableWL.PrefixAlphabet.TotalProgram.bit line 409
  37. theorem OAI.VariableWL.PrefixAlphabet.TotalProgram.prefixCode_number line 411
  38. theorem OAI.VariableWL.PrefixAlphabet.TotalProgram.trim_number line 418
  39. theorem OAI.VariableWL.PrefixAlphabet.TotalProgram.bit_number line 424
  40. def OAI.VariableWL.PrefixDescriptor.Data.roots line 438
  41. def OAI.VariableWL.PrefixDescriptor.Data.anchors line 443
  42. def OAI.VariableWL.PrefixDescriptor.Data.incidence line 447
  43. def OAI.VariableWL.PrefixDescriptor.Data.portData line 451
  44. def OAI.VariableWL.PrefixDescriptor.MatchingGood line 462
  45. theorem OAI.VariableWL.PrefixDescriptor.rootPorts_tree line 466
  46. theorem OAI.VariableWL.PrefixDescriptor.raw_roots line 494