OAI/Computability/MinUncut/PCP/ContextClear.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.Tape line 11
2. def OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.fieldAt line 15
3. def OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.fields line 18
4. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.fieldAt_injective line 20
5. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.fields_length line 27
6. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.fields_nodup line 30
7. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.field_mem line 33
8. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.mem_fields_iff line 38
9. def OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.outputTapes line 46
10. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.output_field line 50
11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.output_frame line 53
12. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.Label line 57
13. def OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.entryLabel line 60
14. def OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.main line 64
15. def OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.program line 68
16. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.entryLabel_eq line 73
17. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.entry_eq line 80
18. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.finalTapes_eq line 84
19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.lengthSum_update line 90
20. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.steps_eq_of_nodup line 100
21. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.trace_trans line 112
22. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.clearTrace line 116
23. def OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.clearInTime line 128
24. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.lengthSum_le_selected line 136
25. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.clauseField_length_le line 148
26. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.variables_add_two_le_input line 156
27. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.loaded_field_length_le line 163
28. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.loaded_cost_le line 172
29. def OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.clearLoadedInTime line 185
30. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.output_loaded_eq_base line 197
31. def OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.clearLoadedToBaseInTime line 208
32. def OAI.MinUncutGames.Foundations.Hastad.SourceContextClear.machine line 218
33. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.prod_decode_pair line 235
34. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.prod_decode_mk line 243
35. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate_prod line 259
36. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.map_enumerate_prod line 274
37. theorem OAI.MinUncutGames.Foundations.Hastad.SourceEnumeration.testTapeEncoding_enumerate line 286
38. theorem OAI.MinUncutGames.Foundations.Hastad.SourceEnumeration.sourceIndexEncoding_enumerate line 294
39. theorem OAI.MinUncutGames.Foundations.Hastad.SourceEnumeration.sourceIndexEncoding_map line 305
40. theorem OAI.MinUncutGames.Foundations.Hastad.SourceEnumeration.rawSourceList_eq_nestedLoops line 317
41. theorem OAI.MinUncutGames.Foundations.Hastad.SourceEnumeration.sourceList_eq_nestedLoops line 327
42. theorem OAI.MinUncutGames.Foundations.Hastad.SourceEnumeration.rawSourceList_flatMap line 338