OAI/Computability/Scheduling/EffectiveFamily.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThreeMachine.Structure.Formula.map line 11
2. theorem OAI.ThreeMachine.Structure.Formula.leaves_map line 16
3. theorem OAI.ThreeMachine.Structure.Formula.map_comp line 21
4. theorem OAI.ThreeMachine.Structure.Formula.map_id line 27
5. theorem OAI.ThreeMachine.Structure.Formula.occurrence_representation line 32
6. def OAI.ThreeMachine.Structure.Formula.depthEnum line 63
7. theorem OAI.ThreeMachine.Structure.Formula.mem_depthEnum line 69
8. def OAI.ThreeMachine.Structure.Formula.templates line 96
9. theorem OAI.ThreeMachine.Structure.Formula.mem_templates line 99
10. theorem OAI.ThreeMachine.Structure.Formula.template_representation line 104
11. def OAI.ThreeMachine.Structure.assignments line 120
12. theorem OAI.ThreeMachine.Structure.assignments_length line 124
13. theorem OAI.ThreeMachine.Structure.mem_assignments line 130
14. def OAI.ThreeMachine.Structure.formulaFamily line 142
15. theorem OAI.ThreeMachine.Structure.mem_formulaFamily_iff line 145
16. theorem OAI.ThreeMachine.Structure.formulaFamily_length line 161
17. def OAI.ThreeMachine.Structure.tripleList line 172
18. theorem OAI.ThreeMachine.Structure.mem_tripleList line 177
19. theorem OAI.ThreeMachine.Structure.tripleList_length line 186
20. def OAI.ThreeMachine.Structure.Atomic.alphabet line 192
21. theorem OAI.ThreeMachine.Structure.Atomic.mem_alphabet line 199
22. theorem OAI.ThreeMachine.Structure.Atomic.alphabet_length line 215
23. theorem OAI.ThreeMachine.Structure.Atomic.alphabet_polynomial line 224