OAI/ModelTheory/Choiceless/GaussMachine.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.CPTSeparation.GaussMachine.Reg line 9
  2. instance OAI.CPTSeparation.GaussMachine.(instance at line 13) line 13
  3. structure OAI.CPTSeparation.GaussMachine.Control line 17
  4. abbrev OAI.CPTSeparation.GaussMachine.Local line 23
  5. abbrev OAI.CPTSeparation.GaussMachine.Prog line 25
  6. structure OAI.CPTSeparation.GaussMachine.Data line 27
  7. def OAI.CPTSeparation.GaussMachine.Data.tapes line 37
  8. lemma OAI.CPTSeparation.GaussMachine.tapes_mat line 46
  9. lemma OAI.CPTSeparation.GaussMachine.tapes_back line 48
  10. lemma OAI.CPTSeparation.GaussMachine.tapes_scan line 50
  11. lemma OAI.CPTSeparation.GaussMachine.tapes_piv line 52
  12. lemma OAI.CPTSeparation.GaussMachine.tapes_pivBack line 54
  13. lemma OAI.CPTSeparation.GaussMachine.tapes_width line 56
  14. lemma OAI.CPTSeparation.GaussMachine.tapes_output line 58
  15. def OAI.CPTSeparation.GaussMachine.st line 60
  16. def OAI.CPTSeparation.GaussMachine._root_.OAI.CPTSeparation.SerialGaussian.Row.entries line 62
  17. lemma OAI.CPTSeparation.GaussMachine.entries_length line 64
  18. lemma OAI.CPTSeparation.GaussMachine.payload_cons line 66
  19. lemma OAI.CPTSeparation.GaussMachine.entries_head_tail line 70
  20. def OAI.CPTSeparation.GaussMachine.scanBody line 77
  21. def OAI.CPTSeparation.GaussMachine.scanLoop line 85
  22. def OAI.CPTSeparation.GaussMachine.scanMatrix line 87
  23. lemma OAI.CPTSeparation.GaussMachine.scanBody_skip line 89
  24. def OAI.CPTSeparation.GaussMachine.ctrl line 123
  25. lemma OAI.CPTSeparation.GaussMachine.payload_head line 125
  26. lemma OAI.CPTSeparation.GaussMachine.scanLoop_nonzero line 130
  27. lemma OAI.CPTSeparation.GaussMachine.scanBody_pick line 142
  28. def OAI.CPTSeparation.GaussMachine.pivotHead line 180
  29. def OAI.CPTSeparation.GaussMachine.pivotTail line 182
  30. lemma OAI.CPTSeparation.GaussMachine.scanLoop_initial line 185
  31. def OAI.CPTSeparation.GaussMachine.findPivot line 209
  32. lemma OAI.CPTSeparation.GaussMachine.pivotTail_length line 214
  33. lemma OAI.CPTSeparation.GaussMachine.findPivot_runs line 218
  34. lemma OAI.CPTSeparation.GaussMachine.entries_reduce line 257
  35. def OAI.CPTSeparation.GaussMachine.reduceInner line 263
  36. def OAI.CPTSeparation.GaussMachine.reduceBody line 269
  37. def OAI.CPTSeparation.GaussMachine.reduceLoop line 276
  38. def OAI.CPTSeparation.GaussMachine.reduceMatrix line 278
  39. def OAI.CPTSeparation.GaussMachine.reducedRow line 280
  40. def OAI.CPTSeparation.GaussMachine.reduceControl line 283
  41. lemma OAI.CPTSeparation.GaussMachine.reduceInner_runs line 286
  42. lemma OAI.CPTSeparation.GaussMachine.reduceBody_runs line 336
  43. lemma OAI.CPTSeparation.GaussMachine.payload_append line 364
  44. lemma OAI.CPTSeparation.GaussMachine.reduceLoop_runs line 367
  45. lemma OAI.CPTSeparation.GaussMachine.reduceMatrix_runs line 388
  46. def OAI.CPTSeparation.GaussMachine.eliminate line 406
  47. def OAI.CPTSeparation.GaussMachine.nextRows line 411
  48. lemma OAI.CPTSeparation.GaussMachine.nextRows_length line 414
  49. lemma OAI.CPTSeparation.GaussMachine.pivot_nonzero line 417
  50. lemma OAI.CPTSeparation.GaussMachine.solve_next line 423
  51. lemma OAI.CPTSeparation.GaussMachine.eliminate_runs line 427
  52. def OAI.CPTSeparation.GaussMachine.normal line 461
  53. lemma OAI.CPTSeparation.GaussMachine.normal_length line 465
  54. lemma OAI.CPTSeparation.GaussMachine.solve_normal line 471
  55. def OAI.CPTSeparation.GaussMachine.eliminationBody line 476
  56. def OAI.CPTSeparation.GaussMachine.eliminationLoop line 479
  57. lemma OAI.CPTSeparation.GaussMachine.eliminationBody_runs line 481
  58. lemma OAI.CPTSeparation.GaussMachine.eliminationLoop_runs line 497
  59. def OAI.CPTSeparation.GaussMachine.zeroBody line 524
  60. def OAI.CPTSeparation.GaussMachine.zeroLoop line 528
  61. def OAI.CPTSeparation.GaussMachine.checkZero line 530
  62. lemma OAI.CPTSeparation.GaussMachine.payload_zero_cons line 535
  63. lemma OAI.CPTSeparation.GaussMachine.zeroLoop_runs line 540
  64. lemma OAI.CPTSeparation.GaussMachine.checkZero_runs line 556
  65. def OAI.CPTSeparation.GaussMachine.solver line 574
  66. lemma OAI.CPTSeparation.GaussMachine.solver_runs line 576