OAI/Analysis/MatrixSigning/Machines/FiniteControl.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CurrentKS.FiniteControl.Registers line 11
2. def OAI.CurrentKS.FiniteControl.guard line 13
3. def OAI.CurrentKS.FiniteControl.whileNonempty line 17
4. lemma OAI.CurrentKS.FiniteControl.step_empty line 20
5. lemma OAI.CurrentKS.FiniteControl.step_nonempty line 31
6. inductive OAI.CurrentKS.FiniteControl.Trace line 46
7. theorem OAI.CurrentKS.FiniteControl.run_trace line 53
8. theorem OAI.CurrentKS.FiniteControl.trace_spec line 76
9. theorem OAI.CurrentKS.FiniteControl.sequence_spec line 82