OAI/Analysis/MatrixSigning/Machines/TerminalInputBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W19.TerminalWitnessMachine.entry_length_le_payload line 11
2. theorem OAI.KS.W19.TerminalWitnessMachine.dimension_le_payload line 24
3. theorem OAI.KS.W19.TerminalWitnessMachine.entry_parts_le_payload line 33
4. theorem OAI.KS.W19.TerminalWitnessMachine.payload_spec line 40
5. theorem OAI.KS.W19.TerminalWitnessMachine.unit_payload_spec line 50