OAI/Computability/MinUncut/Graphs/GraphWordCodec.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MinUncut.Costed.GraphCodec.Mode line 12
2. abbrev OAI.MinUncut.Costed.GraphCodec.Mode.enumList line 15
3. theorem OAI.MinUncut.Costed.GraphCodec.Mode.enumList_getElem?_ctorIdx_eq line 18
4. theorem OAI.MinUncut.Costed.GraphCodec.Mode.enumList_nodup line 22
5. instance OAI.MinUncut.Costed.GraphCodec.(instance at line 24) line 24
6. def OAI.MinUncut.Costed.GraphCodec.bitSymbol line 28
7. def OAI.MinUncut.Costed.GraphCodec.next line 30
8. def OAI.MinUncut.Costed.GraphCodec.emit line 45
9. def OAI.MinUncut.Costed.GraphCodec.machine line 52
10. lemma OAI.MinUncut.Costed.GraphCodec.trPosNum_bits line 54
11. lemma OAI.MinUncut.Costed.GraphCodec.trNat_bits line 65
12. lemma OAI.MinUncut.Costed.GraphCodec.done_output line 72
13. lemma OAI.MinUncut.Costed.GraphCodec.header_output line 77
14. lemma OAI.MinUncut.Costed.GraphCodec.threshold_output line 85
15. lemma OAI.MinUncut.Costed.GraphCodec.cells_output line 92
16. lemma OAI.MinUncut.Costed.GraphCodec.output line 113
17. lemma OAI.MinUncut.Costed.GraphCodec.finiteAlphabet line 119
18. def OAI.MinUncut.Costed.GraphCodec.outputsInTime line 122