OAI/Computability/MinUncut/Machines/FramedWordDecoder.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MinUncut.Costed.FrameDecode.Mode line 10
2. abbrev OAI.MinUncut.Costed.FrameDecode.Mode.enumList line 14
3. theorem OAI.MinUncut.Costed.FrameDecode.Mode.enumList_getElem?_ctorIdx_eq line 16
4. theorem OAI.MinUncut.Costed.FrameDecode.Mode.enumList_nodup line 20
5. instance OAI.MinUncut.Costed.FrameDecode.(instance at line 22) line 22
6. def OAI.MinUncut.Costed.FrameDecode.next line 26
7. def OAI.MinUncut.Costed.FrameDecode.symbol line 32
8. def OAI.MinUncut.Costed.FrameDecode.emit line 34
9. def OAI.MinUncut.Costed.FrameDecode.machine line 40
10. lemma OAI.MinUncut.Costed.FrameDecode.finiteAlphabet line 41
11. lemma OAI.MinUncut.Costed.FrameDecode.suffix_output line 43
12. lemma OAI.MinUncut.Costed.FrameDecode.frame_output line 49
13. lemma OAI.MinUncut.Costed.FrameDecode.output_spec line 58
14. def OAI.MinUncut.Costed.FrameDecode.outputs line 62
15. lemma OAI.MinUncut.Costed.FrameDecode.count_symbols line 68
16. lemma OAI.MinUncut.Costed.FrameDecode.magnitude_symbols line 73