OAI/Analysis/MatrixSigning/Machines/ControllerRuntime.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W17.FixedPSD.originalControllerStepBound line 13
2. def OAI.KS.W17.FixedPSD.originalControllerBound line 17
3. theorem OAI.KS.W17.FixedPSD.ControllerReachable.controller_ticks_le line 19
4. theorem OAI.KS.W17.FixedPSD.controller_original_spec line 49
5. theorem OAI.KS.W17.FixedPSD.controller_payload_spec line 56