OAI/ModelTheory/Choiceless/Matrix.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CPTSeparation.MatrixProgram.Control line 11
  2. abbrev OAI.CPTSeparation.MatrixProgram.Prog line 18
  3. def OAI.CPTSeparation.MatrixProgram.ctrl line 22
  4. def OAI.CPTSeparation.MatrixProgram.memberCode line 24
  5. def OAI.CPTSeparation.MatrixProgram.coefficientStep line 28
  6. def OAI.CPTSeparation.MatrixProgram.coefficientCode line 35
  7. def OAI.CPTSeparation.MatrixProgram.incidentStepX line 38
  8. def OAI.CPTSeparation.MatrixProgram.incidentStepA line 44
  9. def OAI.CPTSeparation.MatrixProgram.incidentCode line 47
  10. def OAI.CPTSeparation.MatrixProgram.normColumn line 49
  11. def OAI.CPTSeparation.MatrixProgram.lambdaColumn line 53
  12. def OAI.CPTSeparation.MatrixProgram.muColumn line 57
  13. def OAI.CPTSeparation.MatrixProgram.normRowCode line 62
  14. def OAI.CPTSeparation.MatrixProgram.consRowCode line 70
  15. def OAI.CPTSeparation.MatrixProgram.program line 80
  16. lemma OAI.CPTSeparation.MatrixProgram.program_wf line 85
  17. def OAI.CPTSeparation.MatrixProgram.member line 90
  18. def OAI.CPTSeparation.MatrixProgram.contribution line 92
  19. def OAI.CPTSeparation.MatrixProgram.coefficient line 96
  20. def OAI.CPTSeparation.MatrixProgram.edgeTest line 99
  21. def OAI.CPTSeparation.MatrixProgram.incident line 102
  22. def OAI.CPTSeparation.MatrixProgram.normChunk line 105
  23. def OAI.CPTSeparation.MatrixProgram.consActive line 109
  24. def OAI.CPTSeparation.MatrixProgram.consChunk line 112
  25. def OAI.CPTSeparation.MatrixProgram.matrix line 116
  26. lemma OAI.CPTSeparation.MatrixProgram.interp_seq line 126
  27. lemma OAI.CPTSeparation.MatrixProgram.interp_load line 129
  28. lemma OAI.CPTSeparation.MatrixProgram.interp_cell line 132
  29. lemma OAI.CPTSeparation.MatrixProgram.interp_emit line 135
  30. lemma OAI.CPTSeparation.MatrixProgram.memberCode_spec line 138
  31. lemma OAI.CPTSeparation.MatrixProgram.coefficientStep_spec line 141
  32. lemma OAI.CPTSeparation.MatrixProgram.coefficient_fold_spec line 148
  33. lemma OAI.CPTSeparation.MatrixProgram.coefficientCode_spec line 162
  34. lemma OAI.CPTSeparation.MatrixProgram.incidentStepX_spec line 168
  35. lemma OAI.CPTSeparation.MatrixProgram.incident_fold_x line 172
  36. lemma OAI.CPTSeparation.MatrixProgram.incidentStepA_spec line 186
  37. lemma OAI.CPTSeparation.MatrixProgram.incident_fold_a line 194
  38. lemma OAI.CPTSeparation.MatrixProgram.incidentCode_spec line 209
  39. lemma OAI.CPTSeparation.MatrixProgram.normColumn_spec line 216
  40. lemma OAI.CPTSeparation.MatrixProgram.lambdaColumn_spec line 222
  41. lemma OAI.CPTSeparation.MatrixProgram.muColumn_spec line 229
  42. lemma OAI.CPTSeparation.MatrixProgram.normRowCode_spec line 233
  43. lemma OAI.CPTSeparation.MatrixProgram.consRowCode_spec line 245
  44. lemma OAI.CPTSeparation.MatrixProgram.program_spec line 260
  45. lemma OAI.CPTSeparation.MatrixProgram.range_eq_finRange_map line 280
  46. lemma OAI.CPTSeparation.MatrixProgram.range_map_eq line 286
  47. lemma OAI.CPTSeparation.MatrixProgram.range_flatMap_eq line 291
  48. lemma OAI.CPTSeparation.MatrixProgram.ofFn_addCases line 295
  49. lemma OAI.CPTSeparation.MatrixProgram.sum_scalar_three line 302
  50. lemma OAI.CPTSeparation.MatrixProgram.contribution_eq line 316
  51. lemma OAI.CPTSeparation.MatrixProgram.coefficient_eq_ordered line 322
  52. lemma OAI.CPTSeparation.MatrixProgram.incident_eq_ordered line 326
  53. lemma OAI.CPTSeparation.MatrixProgram.normChunk_eq line 330
  54. lemma OAI.CPTSeparation.MatrixProgram.consActive_eq line 342
  55. lemma OAI.CPTSeparation.MatrixProgram.consChunk_eq line 347
  56. lemma OAI.CPTSeparation.MatrixProgram.matrix_eq_payload line 360
  57. lemma OAI.CPTSeparation.MatrixProgram.matrix_input line 367