OAI/Analysis/MatrixSigning/Machines/Deterministic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W29.Deterministic.CoinIndependent line 10
2. theorem OAI.KS.W29.Deterministic.coinIndependent_compile line 13
3. theorem OAI.KS.W29.Deterministic.run_eq_of_length_eq line 28
4. theorem OAI.KS.W29.Deterministic.run_eq_false line 44
5. theorem OAI.KS.W29.Deterministic.activeFor_iff_of_length_eq line 49
6. theorem OAI.KS.W29.Deterministic.haltsAfter_iff_of_length_eq line 67
7. theorem OAI.KS.W29.Deterministic.exists_uniform_first_halt line 73
8. theorem OAI.KS.W29.Deterministic.exists_uniform_first_halt_output line 87
9. theorem OAI.KS.W29.Deterministic.activeFor_not_halted_take line 111
10. theorem OAI.KS.W29.Deterministic.first_halt_length_unique line 123
11. theorem OAI.KS.W29.Deterministic.coinIndependent_compose line 137