OAI/Computability/MatchingCount/PairRoutine.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryMatching.StackCode.PairRegisters.left line 12
2. def OAI.BinaryMatching.StackCode.PairRegisters.right line 13
3. def OAI.BinaryMatching.StackCode.PairRegisters.aux line 14
4. lemma OAI.BinaryMatching.StackCode.PairRegisters.left_zero line 16
5. lemma OAI.BinaryMatching.StackCode.PairRegisters.left_inj line 17
6. lemma OAI.BinaryMatching.StackCode.PairRegisters.right_inj line 20
7. lemma OAI.BinaryMatching.StackCode.PairRegisters.left_ne_right line 25
8. lemma OAI.BinaryMatching.StackCode.PairRegisters.left_ne_aux line 31
9. lemma OAI.BinaryMatching.StackCode.PairRegisters.right_ne_aux line 37
10. lemma OAI.BinaryMatching.StackCode.PairRegisters.zero_ne_right line 43
11. lemma OAI.BinaryMatching.StackCode.PairRegisters.zero_ne_aux line 45
12. def OAI.BinaryMatching.StackCode.Routine.pair line 53