OAI/Combinatorics/VariableWL/Binary.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VariableWL.Binary.Digits line 9
  2. def OAI.VariableWL.Binary.number line 11
  3. theorem OAI.VariableWL.Binary.number_lt line 15
  4. theorem OAI.VariableWL.Binary.number_injective line 24
  5. theorem OAI.VariableWL.Binary.number_false line 40
  6. theorem OAI.VariableWL.Binary.number_true line 45
  7. def OAI.VariableWL.Binary.equivalence line 50
  8. theorem OAI.VariableWL.Binary.equivalence_val line 54
  9. def OAI.VariableWL.Binary.domain line 56
  10. def OAI.VariableWL.Binary.table line 59
  11. def OAI.VariableWL.Binary.Allowed line 61
  12. def OAI.VariableWL.Binary.flip line 63
  13. theorem OAI.VariableWL.Binary.domain_nonempty line 65
  14. theorem OAI.VariableWL.Binary.table_injective line 69
  15. theorem OAI.VariableWL.Binary.allowed_iff line 76
  16. theorem OAI.VariableWL.Binary.allowed_unique line 89
  17. theorem OAI.VariableWL.Binary.exists_allowed line 102
  18. theorem OAI.VariableWL.Binary.number_flip line 119
  19. theorem OAI.VariableWL.Binary.number_borrow line 147
  20. def OAI.VariableWL.Binary.cyclicDomain line 175
  21. def OAI.VariableWL.Binary.cyclicTable line 178
  22. def OAI.VariableWL.Binary.CyclicAllowed line 181
  23. def OAI.VariableWL.Binary.cyclicFlip line 184
  24. theorem OAI.VariableWL.Binary.cyclicDomain_nonempty line 186
  25. theorem OAI.VariableWL.Binary.cyclicTable_injective line 192
  26. theorem OAI.VariableWL.Binary.cyclicAllowed_none line 198
  27. theorem OAI.VariableWL.Binary.exists_cyclicAllowed line 203
  28. theorem OAI.VariableWL.Binary.cyclicAllowed_unique line 209
  29. theorem OAI.VariableWL.Binary.cyclic_increment line 229
  30. theorem OAI.VariableWL.Binary.cyclic_decrement line 243
  31. def OAI.VariableWL.Binary.GreaterAt line 266
  32. theorem OAI.VariableWL.Binary.number_lt_iff line 269
  33. def OAI.VariableWL.Binary.thresholdDomain line 317
  34. def OAI.VariableWL.Binary.ThresholdAllowed line 322
  35. theorem OAI.VariableWL.Binary.thresholdDomain_nonempty line 325
  36. theorem OAI.VariableWL.Binary.threshold_none line 331
  37. theorem OAI.VariableWL.Binary.threshold_some line 335
  38. theorem OAI.VariableWL.Binary.threshold_exact line 349
  39. theorem OAI.VariableWL.Binary.threshold_count line 362
  40. def OAI.VariableWL.Circuit.mapGate line 373
  41. def OAI.VariableWL.Circuit.mapPort line 375
  42. theorem OAI.VariableWL.Circuit.System.TrueGate.map line 380