module Evidence where
open import Data.Product
open import Notation
open import Contexts
open C-Global
open C-TopˍLevel

module E-OrdinaryˍOperation(t : Time) where
  open C-OrdinaryˍOperation t

  module E-DailyˍRoutineˍOperation where
    open C-RoutineˍOperation
    postulate
      operationˍsheets-ref         : OperationˍSheets
      dailyˍinspectionˍreports-ref : DailyˍInspectionˍReports
      trainingˍreports-ref         : TrainingˍReports

  module E-ChangeˍMonitoring where
    open C-ChangeˍMonitoring
    postulate
      changeˍdetection-auditˍresult-ref
        :  Purpose/EnviromentˍChangeˍDetection ⟩FunctionˍEvidenceˍAuditˍResult
      changeˍdetection-functionalˍdesignˍdocument-ref
        :  Purpose/EnviromentˍChangeˍDetection ⟩FunctionalˍDesignˍDocument
      changeˍdetection-functionˍimplementationˍrecord-ref
        :  Purpose/EnviromentˍChangeˍDetection ⟩FunctionˍImplementationˍRecord
      changeˍdetection-functionˍtestˍreport-ref
        :  Purpose/EnviromentˍChangeˍDetection ⟩FunctionˍTestˍReport
      changeˍdetection-functionˍoperationˍlog-ref
        :  Purpose/EnviromentˍChangeˍDetection ⟩FunctionˍOperationˍLog

      caˍactivation-auditˍresult-ref
        :  ChangeˍAccommodationˍActivation ⟩FunctionˍEvidenceˍAuditˍResult
      caˍactivation-functionalˍdesignˍdocument-ref
        :  ChangeˍAccommodationˍActivation ⟩FunctionalˍDesignˍDocument
      caˍactivation-functionˍimplementationˍrecord-ref
        :  ChangeˍAccommodationˍActivation ⟩FunctionˍImplementationˍRecord
      caˍactivation-functionˍtestˍreport-ref
        :  ChangeˍAccommodationˍActivation ⟩FunctionˍTestˍReport
      caˍactivation-functionˍoperationˍlog-ref
        :  ChangeˍAccommodationˍActivation ⟩FunctionˍOperationˍLog

  module E-FailureˍMonitoring where
    open C-FailureˍMonitoring
    postulate
      failureˍdetection-auditˍresult-ref
        :  Failure/Failure-PrecursorˍDetection ⟩FunctionˍEvidenceˍAuditˍResult
      failureˍdetection-functionalˍdesignˍdocument-ref
        :  Failure/Failure-PrecursorˍDetection ⟩FunctionalˍDesignˍDocument
      failureˍdetection-functionˍimplementationˍrecord-ref
        :  Failure/Failure-PrecursorˍDetection ⟩FunctionˍImplementationˍRecord
      failureˍdetection-functionˍtestˍreport-ref
        :  Failure/Failure-PrecursorˍDetection ⟩FunctionˍTestˍReport
      failureˍdetection-functionˍoperationˍlog-ref
        :  Failure/Failure-PrecursorˍDetection ⟩FunctionˍOperationˍLog

      frˍactivation-auditˍresult-ref
        :  FailureˍResponseˍActivation ⟩FunctionˍEvidenceˍAuditˍResult
      frˍactivation-functionalˍdesignˍdocument-ref
        :  FailureˍResponseˍActivation ⟩FunctionalˍDesignˍDocument
      frˍactivation-functionˍimplementationˍrecord-ref
        :  FailureˍResponseˍActivation ⟩FunctionˍImplementationˍRecord
      frˍactivation-functionˍtestˍreport-ref
        :  FailureˍResponseˍActivation ⟩FunctionˍTestˍReport
      frˍactivation-functionˍoperationˍlog-ref
        :  FailureˍResponseˍActivation ⟩FunctionˍOperationˍLog

module E-ChangeˍAccommodation(t : Time) where
  open C-ChangeˍAccommodation t
  postulate
    procedrualˍdocˍforˍChangeˍAccommodation
      : ProceduralˍDocˍforˍChangeˍAccommodation
    proceduralˍdocˍforˍAAˍinˍCA
      : ProceduralˍDocˍforˍAAˍinˍCA
  proc-CA = (  procedrualˍdocˍforˍChangeˍAccommodation
            ,′ proceduralˍdocˍforˍAAˍinˍCA)
  postulate
    appropriatenessˍevidence-ref : proc-CA is Appropriate
    executionˍevidence-ref       : proc-CA is Performed

module E-FailureˍResponse(t : Time) where
  open C-FailureˍResponse t

  module E-Plannedˍfor where
    open C-Plannedˍfor
    postulate
      failureˍspecificˍresponseˍplans-ref : FailureˍSpecificˍResponseˍPlans
      proceduralˍdocˍforˍAAˍinˍFRᴾ-ref
        : ProceduralˍDocˍforˍAAˍinˍFRᴾ
    proc-FRᵖ = (  failureˍspecificˍresponseˍplans-ref
               ,′ proceduralˍdocˍforˍAAˍinˍFRᴾ-ref)
    postulate
      appropriatenessˍevidence-ref : proc-FRᵖ is Appropriate
      executionˍevidence-ref       : proc-FRᵖ is Performed

  module E-NotˍPlannedˍfor where
    open C-NotˍPlannedˍfor
    postulate
      proceduralˍdocˍforˍFailureˍResponse⟨NotˍPlannedˍfor⟩
        : ProceduralˍDocˍforˍFailureˍResponse⟨NotˍPlannedˍfor⟩
      proceduralˍdocˍforˍAAˍinˍFRⁿᵖ-ref
        : ProceduralˍDocˍforˍAAˍinˍFR⟨NotˍPlannedˍfor⟩
    proc-FRⁿᵖ =
      (  proceduralˍdocˍforˍFailureˍResponse⟨NotˍPlannedˍfor⟩
      ,′ proceduralˍdocˍforˍAAˍinˍFRⁿᵖ-ref)

    postulate
      appropriatenessˍevidence-ref : proc-FRⁿᵖ is Appropriate
      executionˍevidence-ref       : proc-FRⁿᵖ is Performed

  module E-Unforeseeable where
    open C-Unforeseeable
    postulate
      proceduralˍdocˍforˍFailureˍResponse⟨Unforeseeable⟩
        : ProceduralˍDocˍforˍFailureˍResponse⟨Unforeseeable⟩
      proceduralˍdocˍforˍAAˍinˍFRᵘᶠ
        : ProceduralˍDocˍforˍAAˍinˍFR⟨Unforeseeable⟩
    proc-FR = (  proceduralˍdocˍforˍFailureˍResponse⟨Unforeseeable⟩
              ,′ proceduralˍdocˍforˍAAˍinˍFRᵘᶠ)
    postulate
      appropriatenessˍevidence-ref : proc-FR is Appropriate
      executionˍevidence-ref       : proc-FR is Performed