GV69 assurance

GV69 is statically satisfied by a roadmap constructed as one finished phase, exactly one active phase, and one future phase using the governed ■/▣/□ notation.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV69 where

open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.Identifier using (P; GV)
open import Govenv.Kernel.Roadmap using
  (Roadmap; roadmapOf; _■; _▣; _□; _◇; _×; _╟_)

Proposition : Set
Proposition = Roadmap

proof : Proposition
proof = roadmapOf (
    ((P 0 "assurance-finished" ■) (GV 900 "closed" ×))
  ╟ ((P 1 "assurance-active" ▣) (GV 901 "active" ◇))
  ╟ ((P 2 "assurance-future" □) (GV 902 "future" ◇)))

evidence : StaticEvidence 69
evidence = staticEvidence Proposition proof