OAI/Analysis/MatrixSigning/Realization/ArithmeticRoutine.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CurrentKS.ArithmeticRoutine.encode line 12
2. def OAI.CurrentKS.ArithmeticRoutine.decodeLeft line 14
3. def OAI.CurrentKS.ArithmeticRoutine.program line 16
4. lemma OAI.CurrentKS.ArithmeticRoutine.decode_spec line 20
5. lemma OAI.CurrentKS.ArithmeticRoutine.prepend_spec line 27
6. lemma OAI.CurrentKS.ArithmeticRoutine.extract_spec line 35
7. def OAI.CurrentKS.ArithmeticRoutine.ticks line 43
8. lemma OAI.CurrentKS.ArithmeticRoutine.program_spec line 47
9. def OAI.CurrentKS.ArithmeticRoutine.routine line 55