GV52 is statically satisfied by the roadmap integrity predicate rejecting each governed invalid shape and accepting the corresponding valid phase chain.
{-# OPTIONS --safe #-}
module Govenv.Assurance.GV52 where
open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.Identifier using (P; GV)
open import Govenv.Kernel.Roadmap using
(roadmapIntegrity; _■; _▣; _□; _◇; _×; _├_; _╟_)
record Proposition : Set where
constructor satisfied
field
duplicateGovernanceRejected :
roadmapIntegrity
((P 1 "active" ▣)
((GV 10 "duplicate" ◇) ├ (GV 10 "duplicate" ◇))) ≡ false
backwardsPhaseRejected :
roadmapIntegrity
(((P 2 "active" ▣) (GV 20 "active" ◇))
╟ ((P 1 "future" □) (GV 21 "future" ◇))) ≡ false
unfinishedFinishedPhaseRejected :
roadmapIntegrity
(((P 0 "finished" ■) (GV 30 "pending" ◇))
╟ ((P 1 "active" ▣) (GV 31 "active" ◇))) ≡ false
validProgressionAccepted :
roadmapIntegrity
(((P 0 "finished" ■) (GV 40 "closed" ×))
╟ ((P 1 "active" ▣) (GV 41 "active" ◇))
╟ ((P 2 "future" □) (GV 42 "future" ◇))) ≡ true
proof : Proposition
proof = satisfied refl refl refl refl
evidence : StaticEvidence 52
evidence = staticEvidence Proposition proof