import PhysicsLogic.Philosophy.Observer

open PhysicsLogic.Philosophy.Observer

universe u v
variable {System : Type u} {Regime : Type v}

section Physical
variable (context : PhysicalObserverRoleContext System Regime)
variable (observer : System) (regime : Regime)

example : context.PhysicalObserverAt observer regime =
    (context.observerSystemAt observer regime /\ context.physicalSystemAt observer regime) := rfl

example : context.AllObserversPhysicalAt regime =
    (forall system, context.observerSystemAt system regime -> context.physicalSystemAt system regime) := rfl

example : context.ObserverScopeInhabitedAt regime =
    (exists system, context.observerSystemAt system regime) := rfl

example : context.NonvacuousAllObserversPhysicalAt regime =
    ((forall system, context.observerSystemAt system regime -> context.physicalSystemAt system regime) /\
      exists system, context.observerSystemAt system regime) := rfl
end Physical

section Classified
variable (context : ObserverRoleContext System Regime)
variable (observer : System) (regime : Regime)

example : context.toPhysicalObserverRoleContext.physicalSystemAt = context.physicalSystemAt := rfl
example : context.toPhysicalObserverRoleContext.observerSystemAt = context.observerSystemAt := rfl

example : context.PhysicalObserverAt observer regime =
    (context.observerSystemAt observer regime /\ context.physicalSystemAt observer regime) := rfl

example : context.AllObserversPhysicalAt regime =
    (forall system, context.observerSystemAt system regime -> context.physicalSystemAt system regime) := rfl

example : context.ObserverScopeInhabitedAt regime =
    (exists system, context.observerSystemAt system regime) := rfl

example : context.NonvacuousAllObserversPhysicalAt regime =
    ((forall system, context.observerSystemAt system regime -> context.physicalSystemAt system regime) /\
      exists system, context.observerSystemAt system regime) := rfl
end Classified