OAI/Computability/RationalHitting/ListProcedures.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.Procedure.padEmpty line 10
  2. def OAI.RationalHitting.StackLanguage.Procedure.wordEmpty line 35
  3. theorem OAI.RationalHitting.StackLanguage.Feasible.listUncons line 67
  4. theorem OAI.RationalHitting.StackLanguage.Feasible.listTail line 81
  5. theorem OAI.RationalHitting.StackLanguage.Feasible.listHeadD line 84
  6. theorem OAI.RationalHitting.StackLanguage.Feasible.listEmpty line 87
  7. lemma OAI.RationalHitting.StackLanguage.listCode_tail_le line 98
  8. lemma OAI.RationalHitting.StackLanguage.listCode_iterate_tail_le line 102
  9. theorem OAI.RationalHitting.StackLanguage.Poly.listTail line 113
  10. theorem OAI.RationalHitting.StackLanguage.Poly.listHeadD line 115
  11. theorem OAI.RationalHitting.StackLanguage.Poly.listEmpty line 117
  12. theorem OAI.RationalHitting.StackLanguage.Poly.iterate line 119
  13. theorem OAI.RationalHitting.StackLanguage.Poly.listDrop line 126
  14. theorem OAI.RationalHitting.StackLanguage.Poly.listGetD line 138
  15. def OAI.RationalHitting.StackLanguage.recordCount line 150

    Source documentation

    Count record delimiters, skipping both the escape bit and payload bit.

    def recordCount : List Bool → ℕ
  | [] => 0
  | true::w => recordCount w+1
  | false::[] => 0
  | false::_::w => recordCount w
  16. lemma OAI.RationalHitting.StackLanguage.recordCount_false line 156
  17. def OAI.RationalHitting.StackLanguage.countRecordsBody line 159
  18. def OAI.RationalHitting.StackLanguage.countRecords line 161
  19. lemma OAI.RationalHitting.StackLanguage.drop_both_left line 163
  20. lemma OAI.RationalHitting.StackLanguage.push_both_right line 167
  21. lemma OAI.RationalHitting.StackLanguage.eval_countRecords line 171
  22. lemma OAI.RationalHitting.StackLanguage.recordCount_codeWord line 201
  23. lemma OAI.RationalHitting.StackLanguage.recordCount_listCode line 207
  24. def OAI.RationalHitting.StackLanguage.Procedure.listLength line 215
  25. theorem OAI.RationalHitting.StackLanguage.Poly.listLength line 235
  26. lemma OAI.RationalHitting.StackLanguage.range_map_drop_headD line 246
  27. theorem OAI.RationalHitting.StackLanguage.Poly.listMap line 259