OAI/Combinatorics/EditApproximation/Specification/ConcreteFootprintBridges.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EditApproximation.footprint_cases line 8
  2. theorem OAI.EditApproximation.cases_congr line 16
  3. theorem OAI.EditApproximation.footprint_congr_seven line 25
  4. theorem OAI.EditApproximation.footprint_mpr_congr line 36
  5. def OAI.EditApproximation.groupHeapTransportBridge line 44
  6. def OAI.EditApproximation.groupFootprintTransportBridge line 52
  7. theorem OAI.EditApproximation.footprint_groupTransport line 60
  8. theorem OAI.EditApproximation.heq_decidable_cases_from line 74
  9. theorem OAI.EditApproximation.heq_mpr_both line 122
  10. theorem OAI.EditApproximation.queryInitialGatherHeap_footprint line 151
  11. theorem OAI.EditApproximation.queryBandGatherHeap_footprint line 183
  12. theorem OAI.EditApproximation.queryGroupSourceGatherHeap_footprint line 232
  13. theorem OAI.EditApproximation.queryOnlineSourceGatherHeap_footprint line 283
  14. theorem OAI.EditApproximation.queryLocalRefinementHeap_footprint line 334
  15. theorem OAI.EditApproximation.queryLocalRandomSourcesHeap_footprint line 428
  16. theorem OAI.EditApproximation.queryLocalBandHeap_footprint line 528
  17. theorem OAI.EditApproximation.queryLocalProgramHeap_footprint line 621
  18. theorem OAI.EditApproximation.queryPhysicalTableReadHeap_footprint line 715
  19. theorem OAI.EditApproximation.queryMeanReadHeap_footprint line 738
  20. theorem OAI.EditApproximation.queryPhysicalEarlierReadHeap_footprint line 754
  21. theorem OAI.EditApproximation.queryPhysicalRandomDataRequestHeap_footprint line 804
  22. theorem OAI.EditApproximation.queryPhysicalScalarReadHeap_footprint line 899
  23. def OAI.EditApproximation.scalarGroupFootprintBridge line 912
  24. theorem OAI.EditApproximation.queryPhysicalScalarGroupQueriesHeap_footprint line 937
  25. theorem OAI.EditApproximation.queryPhysicalScalarGroupReadHeap_footprint line 1024
  26. def OAI.EditApproximation.scalarOnlineFootprintBridge line 1039
  27. theorem OAI.EditApproximation.queryPhysicalScalarOnlineReadHeap_footprint line 1057
  28. theorem OAI.EditApproximation.queryFamilyGroupReadHeap_footprint line 1125
  29. theorem OAI.EditApproximation.queryFamilyOnlineReadHeap_footprint line 1147
  30. theorem OAI.EditApproximation.queryRestrictPhysicalBodyHeap_footprint line 1169
  31. theorem OAI.EditApproximation.queryFamilyRefinementHeap_footprint line 1221
  32. theorem OAI.EditApproximation.queryFamilyActiveHeap_footprint line 1286
  33. theorem OAI.EditApproximation.queryFamilyBoundedActiveHeap_footprint line 1349
  34. theorem OAI.EditApproximation.queryInitialConeProgramAtHeap_footprint line 1471
  35. theorem OAI.EditApproximation.queryChargedReadHeap_footprint line 1491
  36. theorem OAI.EditApproximation.queryChargedSeedAtHeap_footprint line 1528
  37. theorem OAI.EditApproximation.queryWarmupProgramHeap_footprint line 1572
  38. theorem OAI.EditApproximation.queryPhysicalInitialHeap_footprint line 1604
  39. theorem OAI.EditApproximation.queryChargedWarmupHeap_footprint line 1659
  40. theorem OAI.EditApproximation.queryChargedFamilyTableHeap_footprint line 1733
  41. theorem OAI.EditApproximation.queryChargedFamilyGlobalHeap_footprint line 1814
  42. theorem OAI.EditApproximation.queryFamilyMemoRawHeap_footprint line 1868
  43. theorem OAI.EditApproximation.computedQueryMemoRawHeap_footprint line 1983
  44. theorem OAI.EditApproximation.computedQueryMemoHeap_footprint line 2327