OAI/Computability/BinPacking/Machines/FrameEmitMachine.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGap.FrameEmitMachine.Alphabet line 12
2. abbrev OAI.BinPackingGap.FrameEmitMachine.State line 13
3. def OAI.BinPackingGap.FrameEmitMachine.finish line 15
4. def OAI.BinPackingGap.FrameEmitMachine.instruction line 19
5. theorem OAI.BinPackingGap.FrameEmitMachine.update_source line 34
6. theorem OAI.BinPackingGap.FrameEmitMachine.update_output line 44
7. theorem OAI.BinPackingGap.FrameEmitMachine.step_nil line 51
8. theorem OAI.BinPackingGap.FrameEmitMachine.step_cons line 61
9. theorem OAI.BinPackingGap.FrameEmitMachine.trace line 71
10. def OAI.BinPackingGap.FrameEmitMachine.inTime line 87