OAI/Combinatorics/VariableWL/CellularCircuit.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Circuit.decodeGates line 12
  2. theorem OAI.VariableWL.Circuit.decodeGates_nonempty line 17
  3. theorem OAI.VariableWL.Circuit.output_decode line 24
  4. theorem OAI.VariableWL.Circuit.input_decode line 30
  5. def OAI.VariableWL.Circuit.encodeGates line 39
  6. theorem OAI.VariableWL.Circuit.encodeGates_nonempty line 45
  7. theorem OAI.VariableWL.Circuit.output_encode line 52
  8. theorem OAI.VariableWL.Circuit.input_encode line 59
  9. theorem OAI.VariableWL.Circuit.const_image line 69
  10. def OAI.VariableWL.Circuit.Description.decodeWitness line 78
  11. def OAI.VariableWL.Circuit.Description.encodedValues line 125
  12. theorem OAI.VariableWL.Circuit.Description.encodedValues_nonempty line 131
  13. def OAI.VariableWL.Circuit.Description.encodeWitness line 141
  14. theorem OAI.VariableWL.Circuit.Description.consistency_iff line 177
  15. abbrev OAI.VariableWL.Circuit.Cellular.Triple line 188
  16. abbrev OAI.VariableWL.Circuit.Cellular.Scalar line 189
  17. abbrev OAI.VariableWL.Circuit.Cellular.And line 190
  18. abbrev OAI.VariableWL.Circuit.Cellular.Edge line 191
  19. structure OAI.VariableWL.Circuit.Cellular.Data line 194
  20. def OAI.VariableWL.Circuit.Cellular.Data.state line 204
  21. def OAI.VariableWL.Circuit.Cellular.Data.source line 208
  22. def OAI.VariableWL.Circuit.Cellular.Data.destination line 213
  23. abbrev OAI.VariableWL.Circuit.Cellular.Data.system line 220
  24. def OAI.VariableWL.Circuit.Cellular.Data.gateMeaning line 240
  25. def OAI.VariableWL.Circuit.Cellular.Data.portMeaning line 248
  26. theorem OAI.VariableWL.Circuit.Cellular.Data.meaningful_edge line 255
  27. theorem OAI.VariableWL.Circuit.Cellular.Data.true_meaning line 267
  28. theorem OAI.VariableWL.Circuit.Cellular.Data.state_true line 290
  29. theorem OAI.VariableWL.Circuit.Cellular.Data.scalar_true_iff line 317
  30. def OAI.VariableWL.Circuit.Cellular.Data.rank line 323
  31. theorem OAI.VariableWL.Circuit.Cellular.Data.rank_increases line 328
  32. theorem OAI.VariableWL.Circuit.Cellular.Data.true_test_iff line 334