OAI/Analysis/MatrixSigning/Machines/ControllerReachable.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.KS.W17.FixedPSD.ControllerReachable line 15
2. theorem OAI.KS.W17.FixedPSD.ControllerReachable.call line 23
3. theorem OAI.KS.W17.FixedPSD.ControllerReachable.matrix_tape_length line 29
4. theorem OAI.KS.W17.FixedPSD.uniform_witness_height line 40
5. theorem OAI.KS.W17.FixedPSD.commonHeight_vector_tape_length line 55
6. theorem OAI.KS.W17.FixedPSD.ControllerReachable.witness_tape_length line 69
7. def OAI.KS.W17.FixedPSD.originalMatrixTapeBound line 81
8. def OAI.KS.W17.FixedPSD.originalWitnessTapeBound line 82
9. def OAI.KS.W17.FixedPSD.originalFrameBound line 83
10. theorem OAI.KS.W17.FixedPSD.ControllerReachable.history_tape_length line 85