OAI/Analysis/MatrixSigning/Machines/FixedStackPortLift.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W01.FixedStack.portPreimage line 10
2. theorem OAI.KS.W01.FixedStack.portPreimage_on_port line 13
3. theorem OAI.KS.W01.FixedStack.portPreimage_off_port line 30
4. def OAI.KS.W01.FixedStack.liftPortsInstruction line 37
5. theorem OAI.KS.W01.FixedStack.liftPortsInstruction_on_port line 43
6. theorem OAI.KS.W01.FixedStack.liftPortsInstruction_off_port line 48
7. def OAI.KS.W01.FixedStack.projectPorts line 53
8. def OAI.KS.W01.FixedStack.liftPortsDispatch line 56
9. def OAI.KS.W01.FixedStack.liftPorts line 61
10. theorem OAI.KS.W01.FixedStack.liftPorts_step line 64
11. theorem OAI.KS.W01.FixedStack.liftPorts_project_step line 75
12. theorem OAI.KS.W01.FixedStack.liftPorts_step_preserves_other line 89
13. theorem OAI.KS.W01.FixedStack.liftPorts_project_run line 102
14. theorem OAI.KS.W01.FixedStack.liftPorts_run_preserves_other line 112
15. theorem OAI.KS.W01.FixedStack.liftPorts_project_init line 122
16. theorem OAI.KS.W01.FixedStack.liftPorts_output_eq line 132
17. theorem OAI.KS.W01.FixedStack.liftPorts_runSeed_state line 140
18. theorem OAI.KS.W01.FixedStack.liftPorts_haltsWithin_iff line 149
19. theorem OAI.KS.W01.FixedStack.liftPorts_successCount_eq line 159
20. theorem OAI.KS.W01.FixedStack.liftPorts_succeedsTwoThirds_iff line 170
21. theorem OAI.KS.W01.FixedStack.liftPorts_polynomialTime_iff line 178
22. def OAI.KS.W29.FixedSequential.liftPorts line 187
23. theorem OAI.KS.W29.FixedSequential.liftPorts_toMachine line 190
24. theorem OAI.KS.W29.FixedSequential.liftPorts_input line 194
25. theorem OAI.KS.W29.FixedSequential.liftPorts_output line 197
26. theorem OAI.KS.W29.FixedSequential.liftPorts_run_state line 200
27. theorem OAI.KS.W29.FixedSequential.activeFor_liftPorts_iff line 208
28. theorem OAI.KS.W29.FixedSequential.haltsAfter_liftPorts_iff line 220
29. theorem OAI.KS.W29.FixedSequential.haltsFromWithin_liftPorts_iff line 227