OAI/Computability/FiniteCompiler/UniformMachines.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Parameterized effective machine realization and uniform finite data.

  1. inductive OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.State line 13
  2. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.machine line 20
  3. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.content line 33
  4. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.marked line 34
  5. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.flat line 35
  6. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.input_ne_blank line 38
  7. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.content_beyond line 45
  8. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.content_before line 50
  9. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.marked_write line 61
  10. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.marked_clear line 86
  11. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.start_step line 95
  12. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.scan_step line 104
  13. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.scan_end line 111
  14. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.scan_run line 119
  15. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.emit_step line 130
  16. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.emit_end line 137
  17. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.emit_run line 143
  18. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.rewind_step line 159
  19. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.rewind_run line 166
  20. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.rewind_end line 173
  21. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.initialize_run line 179
  22. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.lift line 189
  23. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.step_lift line 192
  24. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.lift_respects line 204
  25. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.eval_lift line 212
  26. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.eval_initialized line 217
  27. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.alphabet line 228
  28. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.output_decode line 236
  29. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.initial_view line 244
  30. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.returns_iff line 249
  31. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.lift_returns line 275
  32. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterMachine.realizes line 315
  33. abbrev OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.Control line 348

    Source documentation

    A common, countably coded state space for all unary-initialized programs.

    abbrev Control (Q : Type*) := ℕ ⊕ Q
  34. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.encode line 350
  35. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.decode line 357
  36. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.decode_encode line 364
  37. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.encode_injective line 367
  38. abbrev OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.Cmd line 372
  39. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.encodeCommand line 374
  40. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.transition line 379
  41. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.transition_encode line 389
  42. instance OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.(instance at line 406) line 406
  43. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.primrec_transition line 408
  44. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.support line 450
  45. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.mem_support line 454
  46. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.primrec_support line 457
  47. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.primrec_expand_family line 470

    Source documentation

    Finite weak-component search is primitive recursive uniformly in a primitive-recursive edge table, not just separately at every table.

    theorem primrec_expand_family {r : P → α → α → Bool}
    (hr : Primrec (fun x : P × α × α => r x.1 x.2.1 x.2.2)) :
    Primrec (fun x : P × List α × List α => expand (r x.1) x.2.1 x.2.2) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Effect.Graph.expand

  48. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.primrec_search_family line 485
  49. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.primrec_component_family line 498