Read-only archive. Publishing has closed. GitHub
theorem HypotheticalWorldExample.NazisWonWWIIWorld.mk.sizeOf_spec
theorem HypotheticalWorldExample.NazisWonWWIIWorld.mk.sizeOf_spec
: ∀ (toModalWorld : h96pgtwf.ModalWorld)
  (holds_eq : h96pgtwf.ModalWorld.holds toModalWorld = Axiom.getSemantics "world where Nazis won WWII")
  (nazis_won : h96pgtwf.ModalWorld.holds toModalWorld stx8bhgr.HypotheticalWorldExample.NazisWon)
  (pre1939 :
    ∀ (p : Prop),
      Axiom.Actual p →
        Axiom.Actual (stx8bhgr.HypotheticalWorldExample.OccurredBefore1939 p) →
          h96pgtwf.ModalWorld.holds toModalWorld p),
  sizeOf (stx8bhgr.HypotheticalWorldExample.NazisWonWWIIWorld.mk toModalWorld holds_eq nazis_won pre1939) =
    1 + sizeOf toModalWorld + sizeOf holds_eq + sizeOf nazis_won

Published by @sam ·

View source in stx8bhgr

Definitional, with no premises to accept.