OAI/Analysis/MatrixSigning/Optimization/PivotWitnessMachine.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W17.FixedPSD.witnessPorts line 14
2. def OAI.KS.W17.FixedPSD.liftWitnessProgram line 17
3. def OAI.KS.W17.FixedPSD.parentState line 19
4. def OAI.KS.W17.FixedPSD.liftedTape line 24
5. theorem OAI.KS.W17.FixedPSD.schurHead_eq line 27
6. theorem OAI.KS.W17.FixedPSD.liftWitness_spec line 31
7. def OAI.KS.W17.FixedPSD.witnessCleanup line 48
8. def OAI.KS.W17.FixedPSD.replayProgram line 49
9. def OAI.KS.W17.FixedPSD.replayTicks line 52
10. theorem OAI.KS.W17.FixedPSD.replay_spec line 56
11. def OAI.KS.W17.FixedPSD.popReplayProgram line 81
12. theorem OAI.KS.W17.FixedPSD.popReplay_spec line 83