OAI/Analysis/MatrixSigning/Machines/LiteralProgram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W23.LiteralProgram.push line 9
2. def OAI.KS.W23.LiteralProgram.pushAfter line 13
3. theorem OAI.KS.W23.LiteralProgram.push_spec line 16
4. def OAI.KS.W23.LiteralProgram.program line 33
5. theorem OAI.KS.W23.LiteralProgram.program_spec line 37
6. def OAI.KS.W23.LiteralProgram.pop line 47
7. theorem OAI.KS.W23.LiteralProgram.pop_spec line 51
8. def OAI.KS.W23.LiteralProgram.dropProgram line 68
9. theorem OAI.KS.W23.LiteralProgram.drop_spec line 72