OAI/Analysis/MatrixSigning/Machines/BinaryToUnary.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W03.BinaryToUnary.run_input line 10
2. theorem OAI.KS.W03.BinaryToUnary.run_input_linear line 20
3. theorem OAI.KS.W03.BinaryToUnary.output_correct line 26
4. theorem OAI.KS.W03.BinaryToUnary.halts_within line 33
5. theorem OAI.KS.W03.BinaryToUnary.uniform_binary_to_unary line 41
6. theorem OAI.KS.W03.BinaryToUnary.run_on_ports_budget line 56
7. theorem OAI.KS.W03.BinaryToUnary.run_on_ports line 74
8. theorem OAI.KS.W03.BinaryToUnary.run_on_ports_linear line 83