OAI/MathematicalPhysics/NavierStokes/BalancedTransport/MachineRecursion.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BalancedTransport.Universal.RawInstruction line 10
  2. abbrev OAI.BalancedTransport.Universal.RawMachine line 12
  3. abbrev OAI.BalancedTransport.Universal.RawState line 14
  4. abbrev OAI.BalancedTransport.Universal.RawRun line 16
  5. def OAI.BalancedTransport.Universal.serialize line 18
  6. def OAI.BalancedTransport.Universal.rawBase line 24
  7. def OAI.BalancedTransport.Universal.rawRead line 27
  8. def OAI.BalancedTransport.Universal.rawMove line 30
  9. def OAI.BalancedTransport.Universal.rawStep line 32
  10. def OAI.BalancedTransport.Universal.rawInit line 39
  11. lemma OAI.BalancedTransport.Universal.computable_int_toNat line 44
  12. lemma OAI.BalancedTransport.Universal.computable_int_ofNat line 46
  13. lemma OAI.BalancedTransport.Universal.computable_int_add line 48
  14. lemma OAI.BalancedTransport.Universal.primrec_rawBase line 50
  15. lemma OAI.BalancedTransport.Universal.computable_rawRead line 59
  16. lemma OAI.BalancedTransport.Universal.computable_rawMove line 73
  17. lemma OAI.BalancedTransport.Universal.computable_rawSymbol line 79
  18. lemma OAI.BalancedTransport.Universal.computable_rawInstruction line 92
  19. lemma OAI.BalancedTransport.Universal.computable_rawAdvanceState line 102
  20. lemma OAI.BalancedTransport.Universal.computable_rawAdvance line 117
  21. lemma OAI.BalancedTransport.Universal.computable_rawStep line 127
  22. lemma OAI.BalancedTransport.Universal.computable_rawInit line 130
  23. lemma OAI.BalancedTransport.Universal.rawInit_inputCode line 140
  24. lemma OAI.BalancedTransport.Universal.rawMove_number line 144
  25. lemma OAI.BalancedTransport.Universal.rawBase_initial line 148
  26. lemma OAI.BalancedTransport.Universal.rawRead_append line 157
  27. lemma OAI.BalancedTransport.Universal.serialize_instruction line 161
  28. def OAI.BalancedTransport.Universal.RawRel line 169
  29. lemma OAI.BalancedTransport.Universal.rawRel_initial line 173
  30. lemma OAI.BalancedTransport.Universal.rawStep_rel line 178
  31. lemma OAI.BalancedTransport.Universal.raw_respects line 202
  32. lemma OAI.BalancedTransport.Universal.halts_iff_eval_dom line 213
  33. lemma OAI.BalancedTransport.Universal.raw_eval_dom line 219
  34. lemma OAI.BalancedTransport.Universal.partrec_raw_eval line 224
  35. def OAI.BalancedTransport.Universal.universalPartial line 232
  36. lemma OAI.BalancedTransport.Universal.universalPartial_partrec line 235
  37. lemma OAI.BalancedTransport.Universal.universalPartial_dom line 238
  38. lemma OAI.BalancedTransport.Universal.exists_universal_code line 241