OAI/Analysis/MatrixSigning/Realization/OriginalMachine.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.originalMachine line 10
2. def OAI.CurrentKS.originalMachineTicks line 13
3. lemma OAI.CurrentKS.program_ports_run line 15
4. lemma OAI.CurrentKS.originalMachine_run line 26
5. lemma OAI.CurrentKS.Machine.run_halted line 48
6. theorem OAI.CurrentKS.originalMachine_correct line 55
7. lemma OAI.CurrentKS.deterministic_of_original_cost line 61