Read-only archive. Publishing has closed. GitHub
theorem CapabilityAdditionObservation.mk.injEq
theorem CapabilityAdditionObservation.mk.injEq
: ∀
  (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.