module Argument where
open import Notation
open import Contexts
open import Evidence
open C-Global

main-case = 
  let open C-TopˍLevel in 
  Serviceˍcontinuityˍandˍaccountabilityˍinˍanˍever-changingˍsystemˍcanˍbeˍachieved
  by decompositionˍtoˍtheˍthreeˍelementsˍofˍDEOSˍProcess
     § (Always OrdinaryˍOperationˍstateˍcanˍbeˍachieved
        by argumentˍforˍOrdinaryˍOperation)
     § (Always ChangeˍAccommodationˍCycleˍcanˍbeˍachieved
        by argumentˍforˍChangeˍAccommodation)
     § (Always FailureˍResponseˍCycleˍcanˍbeˍachieved
        by argumentˍforˍFailureˍResponse)
  where
  open C-TopˍLevel

  argumentˍforˍOrdinaryˍOperation
    : (t : Time)  OrdinaryˍOperationˍstateˍcanˍbeˍachieved t
  argumentˍforˍOrdinaryˍOperation t = 
    let open C-OrdinaryˍOperation t
        open E-OrdinaryˍOperation t
    in
    OrdinaryˍOperationˍstateˍcanˍbeˍachieved t
    by decompositionˍbyˍmonitoringˍtargets

       § (let open C-RoutineˍOperation
              open E-DailyˍRoutineˍOperation in
         routineˍoperation is Performed
         by record { operationˍsheets         = operationˍsheets-ref
                   ; dailyˍinspectionˍreports = dailyˍinspectionˍreports-ref
                   ; trainingˍreports         = trainingˍreports-ref })

       § (let open C-ChangeˍMonitoring in
         Monitoringˍforˍchangesˍcanˍbeˍachieved
         by decomposingˍconjunction
            § (Purpose/EnviromentˍChangeˍisˍDetectable
               by argumentˍforˍChangeˍDetection)
            § (ChangeˍAccommodationˍisˍReady
               by argumentˍforˍChangeˍAccommodationˍActivation))

       § (let open C-FailureˍMonitoring in
         Monitoringˍforˍfailuresˍcanˍbeˍachieved
         by decomposingˍconjunction
            § (Failure/Failure-PrecursorˍisˍDetectable
               by argumentˍforˍFailureˍDetection)
            § (FailureˍResponseˍisˍReady
               by argumentˍforˍFailureˍResponseˍActivation))

    where

    argumentˍforˍChangeˍDetection =
      let open C-OrdinaryˍOperation.C-ChangeˍMonitoring t
          open E-OrdinaryˍOperation.E-ChangeˍMonitoring t
      in
      Purpose/EnviromentˍChangeˍisˍDetectable
      by evidenceˍinspection
         § ( Purpose/EnviromentˍChangeˍDetection ⟩FunctionˍEvidenceˍAuditˍResult
            by changeˍdetection-auditˍresult-ref)
         § ( Purpose/EnviromentˍChangeˍDetection ⟩FunctionˍDevelopmentˍEvidence
            by record { functionalˍdesignˍdocument =
                          changeˍdetection-functionalˍdesignˍdocument-ref
                      ; functionˍimplementationˍrecord =
                          changeˍdetection-functionˍimplementationˍrecord-ref
                      ; functionˍtestˍreport =
                          changeˍdetection-functionˍtestˍreport-ref
                      })
         § ( Purpose/EnviromentˍChangeˍDetection ⟩FunctionˍOperationˍLog
            by changeˍdetection-functionˍoperationˍlog-ref)

    argumentˍforˍChangeˍAccommodationˍActivation =
      let open C-OrdinaryˍOperation.C-ChangeˍMonitoring t
          open E-OrdinaryˍOperation.E-ChangeˍMonitoring t
      in
      ChangeˍAccommodationˍisˍReady
      by evidenceˍinspection
         § ( ChangeˍAccommodationˍActivation ⟩FunctionˍEvidenceˍAuditˍResult
            by caˍactivation-auditˍresult-ref)
         § ( ChangeˍAccommodationˍActivation ⟩FunctionˍDevelopmentˍEvidence
            by record { functionalˍdesignˍdocument =
                          caˍactivation-functionalˍdesignˍdocument-ref
                      ; functionˍimplementationˍrecord =
                          caˍactivation-functionˍimplementationˍrecord-ref
                      ; functionˍtestˍreport =
                          caˍactivation-functionˍtestˍreport-ref
                      })
         § ( ChangeˍAccommodationˍActivation ⟩FunctionˍOperationˍLog
            by caˍactivation-functionˍoperationˍlog-ref)

    argumentˍforˍFailureˍDetection =
      let open C-OrdinaryˍOperation.C-FailureˍMonitoring t
          open E-OrdinaryˍOperation.E-FailureˍMonitoring t
      in
      Failure/Failure-PrecursorˍisˍDetectable
      by evidenceˍinspection
         § ( Failure/Failure-PrecursorˍDetection ⟩FunctionˍEvidenceˍAuditˍResult
            by failureˍdetection-auditˍresult-ref)
         § ( Failure/Failure-PrecursorˍDetection ⟩FunctionˍDevelopmentˍEvidence
            by record { functionalˍdesignˍdocument =
                          failureˍdetection-functionalˍdesignˍdocument-ref
                      ; functionˍimplementationˍrecord =
                          failureˍdetection-functionˍimplementationˍrecord-ref
                      ; functionˍtestˍreport =
                          failureˍdetection-functionˍtestˍreport-ref
                      })
         § ( Failure/Failure-PrecursorˍDetection ⟩FunctionˍOperationˍLog
            by failureˍdetection-functionˍoperationˍlog-ref)

    argumentˍforˍFailureˍResponseˍActivation =
      let open C-OrdinaryˍOperation.C-FailureˍMonitoring t
          open E-OrdinaryˍOperation.E-FailureˍMonitoring t
      in
      FailureˍResponseˍisˍReady
      by evidenceˍinspection
         § ( FailureˍResponseˍActivation ⟩FunctionˍEvidenceˍAuditˍResult
            by frˍactivation-auditˍresult-ref)
         § ( FailureˍResponseˍActivation ⟩FunctionˍDevelopmentˍEvidence
            by record { functionalˍdesignˍdocument =
                          frˍactivation-functionalˍdesignˍdocument-ref
                      ; functionˍimplementationˍrecord =
                          frˍactivation-functionˍimplementationˍrecord-ref
                      ; functionˍtestˍreport =
                          frˍactivation-functionˍtestˍreport-ref
                      })
         § ( FailureˍResponseˍActivation ⟩FunctionˍOperationˍLog
            by frˍactivation-functionˍoperationˍlog-ref)

  argumentˍforˍChangeˍAccommodation
    : (t : Time)  ChangeˍAccommodationˍCycleˍcanˍbeˍachieved t
  argumentˍforˍChangeˍAccommodation t =
    let open C-ChangeˍAccommodation t
        open C-System.atTime t
        open E-ChangeˍAccommodation t
    in
    ChangeˍAccommodationˍCycleˍcanˍbeˍachieved t
    by ChangeˍAccommodationˍstage-wiseˍdecomposition
       § (ChangeˍAccommodation-Stage-Goalsˍareˍachieved
          by procedureˍexecution
             § (AppropriateˍProcedureˍisˍPerformed
                by record {
                     proceduralˍdocumentˍforˍTask =
                       procedrualˍdocˍforˍChangeˍAccommodation
                   ; proceduralˍdocumentˍforˍAccountabilityˍAchievement =
                       proceduralˍdocˍforˍAAˍinˍCA
                   ; appropriatenessˍevidence =
                       appropriatenessˍevidence-ref
                   ; executionˍevidence = executionˍevidence-ref
                   }))

  argumentˍforˍFailureˍResponse
    : (t : Time)  FailureˍResponseˍCycleˍcanˍbeˍachieved t
  argumentˍforˍFailureˍResponse t =
    let open C-FailureˍResponse t
        open C-System.atTime t
        open E-FailureˍResponse t
    in
    FailureˍResponseˍCycleˍcanˍbeˍachieved t
    by stage-wiseˍdecomposition
       § (FailureˍResponseˍStage-Goals
          by λ p  
             (failureˍhandledˍin p) is Responded
             by instantiation{x = (failureˍhandledˍin p)}
                § (Every Failure is Responded
                   by decompositionˍbyˍforeseeablity
                      § (let open C-Foreseeable in
                         Responseˍtoˍforeseeableˍfailuresˍcanˍbeˍachieved
                         by argumentˍforˍFailureˍResponse⟨Foreseeable⟩)
                      § (let open C-Unforeseeable in
                         Responseˍtoˍunforeseeableˍfailuresˍcanˍbeˍachieved
                         by argumentˍforˍFailureˍResponse⟨Unforeseeable⟩)))
    where

    argumentˍforˍFailureˍResponse⟨Foreseeable⟩ =
      let open C-FailureˍResponse t
          open C-Foreseeable
      in
      Responseˍtoˍforeseeableˍfailuresˍcanˍbeˍachieved
      by decompositionˍbyˍwhetherˍplannedˍforˍinˍdesignˍorˍnot
         § (let open C-Plannedˍfor in
            Responseˍtoˍfailuresˍplannedˍforˍinˍdesignˍcanˍbeˍachieved
            by argumentˍforˍFailureˍResponse⟨Plannedˍfor⟩)
         § (let open C-NotˍPlannedˍfor in
            Responseˍtoˍfailuresˍnotˍplannedˍforˍinˍdesignˍcanˍbeˍachieved
            by argumentˍforˍFailureˍResponse⟨NotˍPlannedˍfor⟩)
      where

      argumentˍforˍFailureˍResponse⟨Plannedˍfor⟩ =
        let open C-FailureˍResponse.C-Plannedˍfor t
            open E-FailureˍResponse.E-Plannedˍfor t in
        Responseˍtoˍfailuresˍplannedˍforˍinˍdesignˍcanˍbeˍachieved
        by procedureˍexecution
           § (AppropriateˍProcedureˍisˍPerformed
              by record { proceduralˍdocumentˍforˍTask =
                            failureˍspecificˍresponseˍplans-ref
                        ; proceduralˍdocumentˍforˍAccountabilityˍAchievement =
                            proceduralˍdocˍforˍAAˍinˍFRᴾ-ref
                        ; appropriatenessˍevidence =
                            appropriatenessˍevidence-ref
                        ; executionˍevidence = executionˍevidence-ref
                        })

      argumentˍforˍFailureˍResponse⟨NotˍPlannedˍfor⟩ =
        let open C-FailureˍResponse.C-NotˍPlannedˍfor t
            open E-FailureˍResponse.E-NotˍPlannedˍfor t in
        Responseˍtoˍfailuresˍnotˍplannedˍforˍinˍdesignˍcanˍbeˍachieved
        by procedureˍexecution
           § (AppropriateˍProcedureˍisˍPerformed
              by record { proceduralˍdocumentˍforˍTask =
                            proceduralˍdocˍforˍFailureˍResponse⟨NotˍPlannedˍfor⟩
                        ; proceduralˍdocumentˍforˍAccountabilityˍAchievement =
                            proceduralˍdocˍforˍAAˍinˍFRⁿᵖ-ref
                        ; appropriatenessˍevidence =
                            appropriatenessˍevidence-ref
                        ; executionˍevidence = executionˍevidence-ref })

    argumentˍforˍFailureˍResponse⟨Unforeseeable⟩ =
      let open C-FailureˍResponse.C-Unforeseeable t
          open E-FailureˍResponse.E-Unforeseeable t in
      Responseˍtoˍunforeseeableˍfailuresˍcanˍbeˍachieved
      by procedureˍexecution
         § (AppropriateˍProcedureˍisˍPerformed
            by record { proceduralˍdocumentˍforˍTask =
                         proceduralˍdocˍforˍFailureˍResponse⟨Unforeseeable⟩
                      ; proceduralˍdocumentˍforˍAccountabilityˍAchievement =
                         proceduralˍdocˍforˍAAˍinˍFRᵘᶠ
                      ; appropriatenessˍevidence =
                         appropriatenessˍevidence-ref
                      ; executionˍevidence =
                         executionˍevidence-ref })