OAI/Analysis/MatrixSigning/Matrices/SavedPivotPacketMachine.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W08.SavedPivotPacket.frame_at line 13
2. def OAI.KS.W08.SavedPivotPacket.workspace line 41
3. def OAI.KS.W08.SavedPivotPacket.dimPorts line 42
4. def OAI.KS.W08.SavedPivotPacket.packetPorts line 43
5. def OAI.KS.W08.SavedPivotPacket.payload line 44
6. def OAI.KS.W08.SavedPivotPacket.program line 46
7. theorem OAI.KS.W08.SavedPivotPacket.full_spec line 52
8. def OAI.KS.W08.SavedPivotPacket.outerPorts line 92
9. def OAI.KS.W08.SavedPivotPacket.innerPorts line 93
10. def OAI.KS.W08.SavedPivotPacket.popProgram line 94
11. theorem OAI.KS.W08.SavedPivotPacket.pop_spec line 98