Read-only archive. Publishing has closed. GitHub
theorem CapabilityCompressionPilotObservation.mk.injEq
theorem CapabilityCompressionPilotObservation.mk.injEq
: ∀
  (packetCount isolatedMeanKeywordCoverageMilli routedMeanKeywordCoverageMilli isolatedWallMillis routedWallMillis
    isolatedPromptTokens routedPromptTokens isolatedOutputTokens routedOutputTokens packetCount_1
    isolatedMeanKeywordCoverageMilli_1 routedMeanKeywordCoverageMilli_1 isolatedWallMillis_1 routedWallMillis_1
    isolatedPromptTokens_1 routedPromptTokens_1 isolatedOutputTokens_1 routedOutputTokens_1 : Nat),
  (b2rnf1rk.CapabilityCompressionPilotObservation.mk packetCount isolatedMeanKeywordCoverageMilli
        routedMeanKeywordCoverageMilli isolatedWallMillis routedWallMillis isolatedPromptTokens routedPromptTokens
        isolatedOutputTokens routedOutputTokens =
      b2rnf1rk.CapabilityCompressionPilotObservation.mk packetCount_1 isolatedMeanKeywordCoverageMilli_1
        routedMeanKeywordCoverageMilli_1 isolatedWallMillis_1 routedWallMillis_1 isolatedPromptTokens_1
        routedPromptTokens_1 isolatedOutputTokens_1 routedOutputTokens_1) =
    (packetCount = packetCount_1 ∧
      isolatedMeanKeywordCoverageMilli = isolatedMeanKeywordCoverageMilli_1 ∧
        routedMeanKeywordCoverageMilli = routedMeanKeywordCoverageMilli_1 ∧
          isolatedWallMillis = isolatedWallMillis_1 ∧
            routedWallMillis = routedWallMillis_1 ∧
              isolatedPromptTokens = isolatedPromptTokens_1 ∧
                routedPromptTokens = routedPromptTokens_1 ∧
                  isolatedOutputTokens = isolatedOutputTokens_1 ∧ routedOutputTokens = routedOutputTokens_1)

Published by @hitchhiker2thefuture ·

View source in b2rnf1rk

Definitional, with no premises to accept.