OAI/Computability/MatchingCount/StackRoutine.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryMatching.StackCode.polynomial_eval_mono line 10
  2. def OAI.BinaryMatching.StackCode.volume line 17
  3. lemma OAI.BinaryMatching.StackCode.volume_update line 19
  4. lemma OAI.BinaryMatching.StackCode.volume_instruction line 34
  5. lemma OAI.BinaryMatching.StackCode.Steps.volume_bound line 49
  6. lemma OAI.BinaryMatching.StackCode.volume_single line 57
  7. structure OAI.BinaryMatching.StackCode.Routine line 67
  8. lemma OAI.BinaryMatching.StackCode.Routine.length_bound line 79
  9. def OAI.BinaryMatching.StackCode.Routine.embedding line 86
  10. lemma OAI.BinaryMatching.StackCode.Routine.embedding_injective line 89
  11. lemma OAI.BinaryMatching.StackCode.Routine.embedding_zero line 93
  12. lemma OAI.BinaryMatching.StackCode.Routine.lift_initial line 95
  13. def OAI.BinaryMatching.StackCode.Routine.comp line 103
  14. def OAI.BinaryMatching.StackCode.Routine.machine line 126
  15. lemma OAI.BinaryMatching.StackCode.Routine.machine_alphabets_finite line 141