OAI/Combinatorics/MatchingCount/Machines/PhysicalProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.PhysicalStream.Experiment.mean_congr_all line 10
  2. lemma OAI.MatchingFPRAS.PhysicalPost.Implements.map_all line 21
  3. lemma OAI.MatchingFPRAS.PhysicalPost.early_implements line 28
  4. lemma OAI.MatchingFPRAS.PhysicalPost.Implements.early_all line 36
  5. structure OAI.MatchingFPRAS.PhysicalPost.Program line 43
  6. def OAI.MatchingFPRAS.PhysicalPost.Program.seq line 51
  7. def OAI.MatchingFPRAS.PhysicalPost.Program.machine line 58
  8. def OAI.MatchingFPRAS.PhysicalPost.Program.initial line 61
  9. def OAI.MatchingFPRAS.PhysicalPost.Program.final line 62
  10. def OAI.MatchingFPRAS.PhysicalPost.Program.Realizes line 63
  11. def OAI.MatchingFPRAS.PhysicalPost.Program.earlyTapes line 67
  12. lemma OAI.MatchingFPRAS.PhysicalPost.Program.earlyTapes_cost line 69
  13. lemma OAI.MatchingFPRAS.PhysicalPost.Program.Realizes.early line 71
  14. lemma OAI.MatchingFPRAS.PhysicalPost.Program.seq_realizes line 81
  15. def OAI.MatchingFPRAS.PhysicalPost.Program.ofTM1 line 113
  16. lemma OAI.MatchingFPRAS.PhysicalPost.Program.realizes_TM1 line 121