OAI/Analysis/MatrixSigning/Arithmetic/SubtractorSequential.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W19.BinarySubtractor.activeFor_sub line 13
2. theorem OAI.KS.W19.BinarySubtractor.haltsAfter_sub line 60
3. def OAI.KS.W19.BinarySubtractor.reverseMachine line 67
4. def OAI.KS.W19.BinarySubtractor.orientedMachine line 69
5. theorem OAI.KS.W19.BinarySubtractor.run_oriented line 71
6. theorem OAI.KS.W19.BinarySubtractor.run_oriented_correct line 89
7. theorem OAI.KS.W19.BinarySubtractor.oriented_transition_bound line 106