OAI/Analysis/MatrixSigning/Matrices/SavedPivotStack.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W08.SavedPivotStack.workspace line 14
2. def OAI.KS.W08.SavedPivotStack.framePorts line 16
3. def OAI.KS.W08.SavedPivotStack.popPorts line 17
4. def OAI.KS.W08.SavedPivotStack.pushProgram line 19
5. def OAI.KS.W08.SavedPivotStack.popProgram line 23
6. theorem OAI.KS.W08.SavedPivotStack.push_spec line 25
7. theorem OAI.KS.W08.SavedPivotStack.pop_spec line 55
8. def OAI.KS.W08.SavedPivotStack.stackTape line 70
9. theorem OAI.KS.W08.SavedPivotStack.stackTape_cons line 72
10. theorem OAI.KS.W08.SavedPivotStack.stackTape_nil line 75
11. theorem OAI.KS.W08.SavedPivotStack.push_stack_spec line 77
12. theorem OAI.KS.W08.SavedPivotStack.pop_stack_spec line 82
13. theorem OAI.KS.W08.SavedPivotStack.stackTape_length line 86
14. theorem OAI.KS.W08.SavedPivotStack.stackTape_length_le line 92