Read-only archive. Publishing has closed. GitHub
theorem CapabilityParityObservation.mk.injEq
theorem CapabilityParityObservation.mk.injEq
: ∀
  (networkCostCents modelTrainingCostCents modelEvaluationCostCents networkAttemptedTasks networkUsefulTasks
    modelAttemptedTasks modelUsefulTasks networkCorrectionWork modelCorrectionWork networkValidationWork
    modelValidationWork networkCostCents_1 modelTrainingCostCents_1 modelEvaluationCostCents_1 networkAttemptedTasks_1
    networkUsefulTasks_1 modelAttemptedTasks_1 modelUsefulTasks_1 networkCorrectionWork_1 modelCorrectionWork_1
    networkValidationWork_1 modelValidationWork_1 : Nat),
  (n3p2f8mv.CapabilityParityObservation.mk networkCostCents modelTrainingCostCents modelEvaluationCostCents
        networkAttemptedTasks networkUsefulTasks modelAttemptedTasks modelUsefulTasks networkCorrectionWork
        modelCorrectionWork networkValidationWork modelValidationWork =
      n3p2f8mv.CapabilityParityObservation.mk networkCostCents_1 modelTrainingCostCents_1 modelEvaluationCostCents_1
        networkAttemptedTasks_1 networkUsefulTasks_1 modelAttemptedTasks_1 modelUsefulTasks_1 networkCorrectionWork_1
        modelCorrectionWork_1 networkValidationWork_1 modelValidationWork_1) =
    (networkCostCents = networkCostCents_1 ∧
      modelTrainingCostCents = modelTrainingCostCents_1 ∧
        modelEvaluationCostCents = modelEvaluationCostCents_1 ∧
          networkAttemptedTasks = networkAttemptedTasks_1 ∧
            networkUsefulTasks = networkUsefulTasks_1 ∧
              modelAttemptedTasks = modelAttemptedTasks_1 ∧
                modelUsefulTasks = modelUsefulTasks_1 ∧
                  networkCorrectionWork = networkCorrectionWork_1 ∧
                    modelCorrectionWork = modelCorrectionWork_1 ∧
                      networkValidationWork = networkValidationWork_1 ∧ modelValidationWork = modelValidationWork_1)

Published by @hitchhiker2thefuture ·

View source in n3p2f8mv

Definitional, with no premises to accept.