OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Transitions.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistory.due line 14
  2. def OAI.MatrixMultiplication.AllFieldHistory.produced line 21
  3. abbrev OAI.MatrixMultiplication.AllFieldHistory.Carried line 28
  4. abbrev OAI.MatrixMultiplication.AllFieldHistory.Produced line 29
  5. theorem OAI.MatrixMultiplication.AllFieldHistory.produced_not_resident line 31
  6. theorem OAI.MatrixMultiplication.AllFieldHistory.resident_succ_iff line 40
  7. def OAI.MatrixMultiplication.AllFieldHistory.stateTransitionForward line 63
  8. def OAI.MatrixMultiplication.AllFieldHistory.stateTransitionBackward line 75
  9. def OAI.MatrixMultiplication.AllFieldHistory.stateTransition line 80
  10. def OAI.MatrixMultiplication.AllFieldHistory.productionParent line 93
  11. abbrev OAI.MatrixMultiplication.AllFieldHistory.DueState line 110
  12. def OAI.MatrixMultiplication.AllFieldHistory.activeToDue line 112
  13. def OAI.MatrixMultiplication.AllFieldHistory.dueToActive line 122
  14. def OAI.MatrixMultiplication.AllFieldHistory.activeSourceEquiv line 131
  15. def OAI.MatrixMultiplication.AllFieldHistory.bSubdivisionPositionEquiv line 146
  16. theorem OAI.MatrixMultiplication.AllFieldHistory.final_state_terminal line 154