OAI/Analysis/MatrixSigning/Realization/FixedSubroutineBridge.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W29.FixedSequential.lift3_run_state line 11
2. theorem OAI.KS.W29.FixedSequential.activeFor_lift3_iff line 18
3. theorem OAI.KS.W29.FixedSequential.haltsAfter_lift3_iff line 30
4. theorem OAI.KS.W29.FixedSequential.haltsFromWithin_lift3_iff line 40