OAI/MathematicalPhysics/NavierStokes/Material/Compiler.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Alternating.Memory.tapeUpdate line 8
  2. def OAI.Alternating.Memory.branchCode line 15
  3. theorem OAI.Alternating.Memory.branchCode_smooth line 19
  4. def OAI.Alternating.Memory.localBranchCode line 24
  5. theorem OAI.Alternating.Memory.localBranchCode_smooth line 31
  6. def OAI.Alternating.Memory.localWrite line 41
  7. theorem OAI.Alternating.Memory.localWrite_smooth line 51
  8. def OAI.Alternating.Memory.sequenceCode line 69
  9. theorem OAI.Alternating.Memory.sequenceCode_head line 72
  10. theorem OAI.Alternating.Memory.sequenceCode_agree line 77
  11. theorem OAI.Alternating.Memory.sequenceCode_extend line 85
  12. theorem OAI.Alternating.Memory.sequenceCode_widen line 89
  13. theorem OAI.Alternating.Memory.sequenceCode_pop line 98
  14. def OAI.Alternating.Memory.leftSequence line 107
  15. def OAI.Alternating.Memory.rightSequence line 110
  16. theorem OAI.Alternating.Memory.actualSequences_vanish line 113
  17. theorem OAI.Alternating.Memory.leftSequence_moveRight_zero line 119
  18. theorem OAI.Alternating.Memory.leftSequence_moveRight_succ line 124
  19. theorem OAI.Alternating.Memory.rightSequence_moveRight line 131
  20. theorem OAI.Alternating.Memory.leftSequence_stay line 139
  21. theorem OAI.Alternating.Memory.rightSequence_stay_zero line 146
  22. theorem OAI.Alternating.Memory.rightSequence_stay_succ line 150
  23. theorem OAI.Alternating.Memory.leftSequence_moveLeft line 157
  24. theorem OAI.Alternating.Memory.rightSequence_moveLeft_zero line 164
  25. theorem OAI.Alternating.Memory.rightSequence_moveLeft_one line 171
  26. theorem OAI.Alternating.Memory.rightSequence_moveLeft_add_two line 175
  27. theorem OAI.Alternating.Memory.tapeUpdate_correct line 183
  28. theorem OAI.Alternating.Memory.width_succ line 253
  29. theorem OAI.Alternating.Memory.actualBlock_leftCode_eq line 257
  30. theorem OAI.Alternating.Memory.actualBlock_rightCode_eq line 261
  31. theorem OAI.Alternating.Memory.tapeUpdate_actual line 265
  32. theorem OAI.Alternating.Memory.branchCode_actual line 280
  33. theorem OAI.Alternating.Memory.sequenceCode_digit_cylinder line 293
  34. theorem OAI.Alternating.Memory.actualBlock_left_cylinder line 315
  35. theorem OAI.Alternating.Memory.actualBlock_right_cylinder line 325
  36. theorem OAI.Alternating.Memory.branchCode_nonleft line 335
  37. theorem OAI.Alternating.Memory.localBranchCode_exact line 347
  38. theorem OAI.Alternating.Memory.localWrite_at_cylinders line 356
  39. theorem OAI.Alternating.Memory.localWrite_exact line 373