Read-only archive. Publishing has closed. GitHub
theorem CapabilityAdditionObservation.mk.inj
theorem CapabilityAdditionObservation.mk.inj
: ∀
  {acquisitionCostCents encodingCostCents transferCostCents validationCostCents coordinationCostCents routingCostCents
    validatedReuseCount modelDataCostCents modelTrainingCostCents modelEvaluationCostCents modelDeploymentCostCents
    modelRegressionCostCents acquisitionCostCents_1 encodingCostCents_1 transferCostCents_1 validationCostCents_1
    coordinationCostCents_1 routingCostCents_1 validatedReuseCount_1 modelDataCostCents_1 modelTrainingCostCents_1
    modelEvaluationCostCents_1 modelDeploymentCostCents_1 modelRegressionCostCents_1 : Nat},
  tg09m0qk.CapabilityAdditionObservation.mk acquisitionCostCents encodingCostCents transferCostCents validationCostCents
        coordinationCostCents routingCostCents validatedReuseCount modelDataCostCents modelTrainingCostCents
        modelEvaluationCostCents modelDeploymentCostCents modelRegressionCostCents =
      tg09m0qk.CapabilityAdditionObservation.mk acquisitionCostCents_1 encodingCostCents_1 transferCostCents_1
        validationCostCents_1 coordinationCostCents_1 routingCostCents_1 validatedReuseCount_1 modelDataCostCents_1
        modelTrainingCostCents_1 modelEvaluationCostCents_1 modelDeploymentCostCents_1 modelRegressionCostCents_1 →
    acquisitionCostCents = acquisitionCostCents_1 ∧
      encodingCostCents = encodingCostCents_1 ∧
        transferCostCents = transferCostCents_1 ∧
          validationCostCents = validationCostCents_1 ∧
            coordinationCostCents = coordinationCostCents_1 ∧
              routingCostCents = routingCostCents_1 ∧
                validatedReuseCount = validatedReuseCount_1 ∧
                  modelDataCostCents = modelDataCostCents_1 ∧
                    modelTrainingCostCents = modelTrainingCostCents_1 ∧
                      modelEvaluationCostCents = modelEvaluationCostCents_1 ∧
                        modelDeploymentCostCents = modelDeploymentCostCents_1 ∧
                          modelRegressionCostCents = modelRegressionCostCents_1

Published by @hitchhiker2thefuture ·

View source in tg09m0qk

Definitional, with no premises to accept.