OAI/Computability/Scheduling/FamilyRoutines.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThreeMachine.StackCompiler.Uniform.natLT line 15
  2. def OAI.ThreeMachine.StackCompiler.Uniform.finCons line 23
  3. def OAI.ThreeMachine.StackCompiler.Uniform.finEmpty line 26
  4. def OAI.ThreeMachine.StackCompiler.Uniform.assignments line 32
  5. def OAI.ThreeMachine.StackCompiler.Uniform.tripleSet line 38
  6. def OAI.ThreeMachine.StackCompiler.Uniform.triples line 49
  7. def OAI.ThreeMachine.StackCompiler.Uniform.predecessorCount line 63
  8. def OAI.ThreeMachine.StackCompiler.Uniform.predecessors line 69
  9. def OAI.ThreeMachine.StackCompiler.Uniform.rankFromCounts line 73
  10. def OAI.ThreeMachine.StackCompiler.Uniform.rank line 88
  11. def OAI.ThreeMachine.StackCompiler.Uniform.reverseRank line 95
  12. def OAI.ThreeMachine.StackCompiler.coneSet line 106
  13. theorem OAI.ThreeMachine.StackCompiler.atomicCone line 115
  14. theorem OAI.ThreeMachine.StackCompiler.map_finRange_nat line 121
  15. theorem OAI.ThreeMachine.StackCompiler.atomicThreshold line 126
  16. def OAI.ThreeMachine.StackCompiler.Uniform.thresholdSets line 141
  17. def OAI.ThreeMachine.StackCompiler.Uniform.matrixGetFrame line 160
  18. def OAI.ThreeMachine.StackCompiler.Uniform.conePred line 167
  19. def OAI.ThreeMachine.StackCompiler.Uniform.cone line 177
  20. def OAI.ThreeMachine.StackCompiler.Uniform.cones line 194
  21. def OAI.ThreeMachine.StackCompiler.Uniform.ranks line 203
  22. def OAI.ThreeMachine.StackCompiler.Uniform.thresholds line 209
  23. def OAI.ThreeMachine.StackCompiler.Uniform.atomSets line 217
  24. theorem OAI.ThreeMachine.Structure.assignments_map line 234
  25. theorem OAI.ThreeMachine.Structure.Formula.map_evalFinset line 247
  26. theorem OAI.ThreeMachine.Structure.Atomic.filter_eval line 254
  27. theorem OAI.ThreeMachine.Structure.effectiveFamily_eq_finset line 262
  28. def OAI.ThreeMachine.StackCompiler.Uniform.evalTemplate line 280
  29. def OAI.ThreeMachine.StackCompiler.Uniform.evalTemplates line 290
  30. def OAI.ThreeMachine.StackCompiler.Uniform.family line 295
  31. def OAI.ThreeMachine.StackCompiler.Uniform.fullSolveK line 301
  32. def OAI.ThreeMachine.StackCompiler.Uniform.fullSolve line 313