OAI/Analysis/MatrixSigning/Machines/SchurEntryMachine.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W07.SchurEntryMachine.framePorts line 11
2. def OAI.KS.W07.SchurEntryMachine.appendProgram line 12
3. theorem OAI.KS.W07.SchurEntryMachine.append_spec line 15
4. def OAI.KS.W07.SchurEntryMachine.program line 42
5. theorem OAI.KS.W07.SchurEntryMachine.full_spec line 44
6. theorem OAI.KS.W07.SchurEntryMachine.append_reverse_prefix line 62
7. def OAI.KS.W07.SchurEntryMachine.finishProgram line 65
8. theorem OAI.KS.W07.SchurEntryMachine.finish_spec line 68