{-# OPTIONS --cubical #-}
module SemanticExplanation.IndustryCandidateRuns where
open import Agda.Builtin.Equality using (_≡_ ; refl)
open import Agda.Builtin.List using (List ; [] ; _∷_)
open import Agda.Builtin.String using (String)
open import Agda.Primitive using (Set)
open import SemanticExplanation
import SemanticExplanation.Industry.Logic as Logic
import SemanticExplanation.Industry.LogicMore as LogicMore
import SemanticExplanation.Industry.OWL as OWL
import SemanticExplanation.Industry.OWLMore as OWLMore
import SemanticExplanation.Industry.Spartan as Spartan
import SemanticExplanation.Industry.SpartanMore as SpartanMore
import SemanticExplanation.Industry.DiscourseProfiles as Profiles
record CandidateRun : Set where
constructor candidate-run
field
target : String
caseStudy : String
declaration : String
selectedCandidateId : String
canonicalText : String
compactText : String
evidenceText : String
structuredText : String
domainEvidenceText : String
batchReleaseCanonical batchReleaseCompact
batchReleaseEvidence batchReleaseStructured batchReleaseDomain : Explanation
batchReleaseCanonical =
explainName Logic.batchReactorDomain
Logic.pressureVerificationAuthorizesDischarge
batchReleaseCompact =
explainNameSelected Logic.batchReactorDomain "compact/v1"
Logic.pressureVerificationAuthorizesDischarge
batchReleaseEvidence =
explainNameSelected Logic.batchReactorDomain "evidence/v1"
Logic.pressureVerificationAuthorizesDischarge
batchReleaseStructured =
explainNameSelected Logic.batchReactorDomain "structured/v1"
Logic.pressureVerificationAuthorizesDischarge
batchReleaseDomain =
explainNameDomainEvidence Profiles.batchReactorProfile
Logic.batchReactorDomain Logic.pressureVerificationAuthorizesDischarge
batchReleaseFamily : List Explanation
batchReleaseFamily =
explainNameFamily Logic.batchReactorDomain
Logic.pressureVerificationAuthorizesDischarge
batchReleaseCandidateIds
: candidateIds batchReleaseFamily
≡ "canonical/v1" ∷ "compact/v1" ∷ "evidence/v1" ∷ "structured/v1" ∷ []
batchReleaseCandidateIds = refl
batchReleaseCanonicalText
: Explanation.text batchReleaseCanonical
≡ "For every batch-reactor control state releaseCandidate, if releaseCandidate has a reviewed two-transmitter pressure certificate below the discharge-release threshold, then releaseCandidate authorizes the product-discharge valve to open."
batchReleaseCanonicalText = refl
batchReleaseCompactText
: Explanation.text batchReleaseCompact
≡ "For every batch-reactor control state releaseCandidate, if releaseCandidate has a reviewed two-transmitter pressure certificate below the discharge-release threshold, then releaseCandidate authorizes the product-discharge valve to open."
batchReleaseCompactText = refl
batchReleaseEvidenceText
: Explanation.text batchReleaseEvidence
≡ "For every batch-reactor control state releaseCandidate, given releaseCandidate has a reviewed two-transmitter pressure certificate below the discharge-release threshold, releaseCandidate authorizes the product-discharge valve to open."
batchReleaseEvidenceText = refl
batchReleaseStructuredText
: Explanation.text batchReleaseStructured
≡ "For every batch-reactor control state releaseCandidate, the following conditions suffice: releaseCandidate has a reviewed two-transmitter pressure certificate below the discharge-release threshold. Under those conditions, releaseCandidate authorizes the product-discharge valve to open."
batchReleaseStructuredText = refl
batchReleaseDomainText
: Explanation.text batchReleaseDomain
≡ "For every batch-reactor control state, the batch-release authorization basis in declaration order is: Dual-transmitter release-threshold evidence — the release candidate has a reviewed two-transmitter pressure certificate below the discharge-release threshold. Product-discharge authorization — the release candidate authorizes the product-discharge valve to open."
batchReleaseDomainText = refl
railProtectionCanonical railProtectionCompact
railProtectionEvidence railProtectionStructured railProtectionDomain : Explanation
railProtectionCanonical =
explainName LogicMore.logicMoreDomain
LogicMore.provedBarriersProtectRailMovement
railProtectionCompact =
explainNameSelected LogicMore.logicMoreDomain "compact/v1"
LogicMore.provedBarriersProtectRailMovement
railProtectionEvidence =
explainNameSelected LogicMore.logicMoreDomain "evidence/v1"
LogicMore.provedBarriersProtectRailMovement
railProtectionStructured =
explainNameSelected LogicMore.logicMoreDomain "structured/v1"
LogicMore.provedBarriersProtectRailMovement
railProtectionDomain =
explainNameDomainEvidence Profiles.railMovementProfile
LogicMore.logicMoreDomain LogicMore.provedBarriersProtectRailMovement
railProtectionCanonicalText
: Explanation.text railProtectionCanonical
≡ "For every recorded level-crossing movement movement, if movement has both road barriers proved down, then if movement has the road conflict zone proved clear, then movement authorizes the protected rail movement."
railProtectionCanonicalText = refl
railProtectionCompactText
: Explanation.text railProtectionCompact
≡ "For every recorded level-crossing movement movement, if movement has both road barriers proved down and movement has the road conflict zone proved clear, then movement authorizes the protected rail movement."
railProtectionCompactText = refl
railProtectionEvidenceText
: Explanation.text railProtectionEvidence
≡ "For every recorded level-crossing movement movement, given movement has both road barriers proved down; and movement has the road conflict zone proved clear, movement authorizes the protected rail movement."
railProtectionEvidenceText = refl
railProtectionStructuredText
: Explanation.text railProtectionStructured
≡ "For every recorded level-crossing movement movement, the following conditions suffice: movement has both road barriers proved down; and movement has the road conflict zone proved clear. Under those conditions, movement authorizes the protected rail movement."
railProtectionStructuredText = refl
railProtectionDomainText
: Explanation.text railProtectionDomain
≡ "For every recorded level-crossing movement, the protected-movement authority basis in declaration order is: Physical barrier proof — the movement has both road barriers proved down; and Conflict-zone clearance — the movement has the road conflict zone proved clear. Protected-movement authority — the movement authorizes the protected rail movement."
railProtectionDomainText = refl
coldReleaseCanonical coldReleaseCompact
coldReleaseEvidence coldReleaseStructured coldReleaseDomain : Explanation
coldReleaseCanonical =
explainName LogicMore.logicMoreDomain
LogicMore.reviewedStabilityEvidenceAllowsRelease
coldReleaseCompact =
explainNameSelected LogicMore.logicMoreDomain "compact/v1"
LogicMore.reviewedStabilityEvidenceAllowsRelease
coldReleaseEvidence =
explainNameSelected LogicMore.logicMoreDomain "evidence/v1"
LogicMore.reviewedStabilityEvidenceAllowsRelease
coldReleaseStructured =
explainNameSelected LogicMore.logicMoreDomain "structured/v1"
LogicMore.reviewedStabilityEvidenceAllowsRelease
coldReleaseDomain =
explainNameDomainEvidence Profiles.coldChainProfile
LogicMore.logicMoreDomain LogicMore.reviewedStabilityEvidenceAllowsRelease
coldReleaseCanonicalText
: Explanation.text coldReleaseCanonical
≡ "For every temperature-controlled shipment consignment, if consignment must enter quality quarantine, then if consignment has reviewed stability evidence showing acceptable impact, then if consignment has completed quality-unit review, then consignment is eligible for distribution release."
coldReleaseCanonicalText = refl
coldReleaseCompactText
: Explanation.text coldReleaseCompact
≡ "For every temperature-controlled shipment consignment, if consignment must enter quality quarantine, consignment has reviewed stability evidence showing acceptable impact, and consignment has completed quality-unit review, then consignment is eligible for distribution release."
coldReleaseCompactText = refl
coldReleaseEvidenceText
: Explanation.text coldReleaseEvidence
≡ "For every temperature-controlled shipment consignment, given consignment must enter quality quarantine; consignment has reviewed stability evidence showing acceptable impact; and consignment has completed quality-unit review, consignment is eligible for distribution release."
coldReleaseEvidenceText = refl
coldReleaseStructuredText
: Explanation.text coldReleaseStructured
≡ "For every temperature-controlled shipment consignment, the following conditions suffice: consignment must enter quality quarantine; consignment has reviewed stability evidence showing acceptable impact; and consignment has completed quality-unit review. Under those conditions, consignment is eligible for distribution release."
coldReleaseStructuredText = refl
coldReleaseDomainText
: Explanation.text coldReleaseDomain
≡ "For every temperature-controlled shipment, the distribution-release disposition basis in declaration order is: Controlled-hold status — the consignment must enter quality quarantine; Stability-impact assessment — the consignment has reviewed stability evidence showing acceptable impact; and Quality-unit approval — the consignment has completed quality-unit review. Distribution-release disposition — the consignment is eligible for distribution release."
coldReleaseDomainText = refl
mroReleaseCanonical mroReleaseCompact
mroReleaseEvidence mroReleaseStructured mroReleaseDomain : Explanation
mroReleaseCanonical =
explainName OWL.aircraftMaintenanceDomain OWL.returnToServiceEligibility
mroReleaseCompact =
explainNameSelected OWL.aircraftMaintenanceDomain "compact/v1"
OWL.returnToServiceEligibility
mroReleaseEvidence =
explainNameSelected OWL.aircraftMaintenanceDomain "evidence/v1"
OWL.returnToServiceEligibility
mroReleaseStructured =
explainNameSelected OWL.aircraftMaintenanceDomain "structured/v1"
OWL.returnToServiceEligibility
mroReleaseDomain =
explainNameDomainEvidence Profiles.aircraftMroProfile
OWL.aircraftMaintenanceDomain OWL.returnToServiceEligibility
mroReleaseCanonicalText
: Explanation.text mroReleaseCanonical
≡ "For every licensed aircraft engineer certifyingEngineer, for every turbofan engine module engineModule, if certifyingEngineer has a traceable inspection for engineModule, then if engineModule has at least one conforming borescope inspection on record, then if certifyingEngineer holds release authorization for engineModule, then certifyingEngineer is eligible to issue a return-to-service release for engineModule."
mroReleaseCanonicalText = refl
mroReleaseCompactText
: Explanation.text mroReleaseCompact
≡ "For every licensed aircraft engineer certifyingEngineer and every turbofan engine module engineModule, if certifyingEngineer has a traceable inspection for engineModule, engineModule has at least one conforming borescope inspection on record, and certifyingEngineer holds release authorization for engineModule, then certifyingEngineer is eligible to issue a return-to-service release for engineModule."
mroReleaseCompactText = refl
mroReleaseEvidenceText
: Explanation.text mroReleaseEvidence
≡ "For every licensed aircraft engineer certifyingEngineer and every turbofan engine module engineModule, given certifyingEngineer has a traceable inspection for engineModule; engineModule has at least one conforming borescope inspection on record; and certifyingEngineer holds release authorization for engineModule, certifyingEngineer is eligible to issue a return-to-service release for engineModule."
mroReleaseEvidenceText = refl
mroReleaseStructuredText
: Explanation.text mroReleaseStructured
≡ "For every licensed aircraft engineer certifyingEngineer and every turbofan engine module engineModule, the following conditions suffice: certifyingEngineer has a traceable inspection for engineModule; engineModule has at least one conforming borescope inspection on record; and certifyingEngineer holds release authorization for engineModule. Under those conditions, certifyingEngineer is eligible to issue a return-to-service release for engineModule."
mroReleaseStructuredText = refl
mroReleaseDomainText
: Explanation.text mroReleaseDomain
≡ "For every licensed aircraft engineer and every turbofan engine module, the return-to-service release basis in declaration order is: Traceable maintenance record — the certifying engineer has a traceable inspection for the engine module; Mandatory borescope evidence — the engine module has at least one conforming borescope inspection on record; and Engineer release authorization — the certifying engineer holds release authorization for the engine module. Return-to-service disposition — the certifying engineer is eligible to issue a return-to-service release for the engine module."
mroReleaseDomainText = refl
pharmaRecallCanonical pharmaRecallCompact
pharmaRecallEvidence pharmaRecallStructured pharmaRecallDomain : Explanation
pharmaRecallCanonical =
explainName OWLMore.owlMoreDomain OWLMore.batchRecallPropagatesToPack
pharmaRecallCompact =
explainNameSelected OWLMore.owlMoreDomain "compact/v1"
OWLMore.batchRecallPropagatesToPack
pharmaRecallEvidence =
explainNameSelected OWLMore.owlMoreDomain "evidence/v1"
OWLMore.batchRecallPropagatesToPack
pharmaRecallStructured =
explainNameSelected OWLMore.owlMoreDomain "structured/v1"
OWLMore.batchRecallPropagatesToPack
pharmaRecallDomain =
explainNameDomainEvidence Profiles.medicineRecallProfile
OWLMore.owlMoreDomain OWLMore.batchRecallPropagatesToPack
pharmaRecallCanonicalText
: Explanation.text pharmaRecallCanonical
≡ "For every serialized medicine pack pack, for every production batch lot, for every market recall recall, if pack belongs to lot, then if lot is included in recall, then pack is affected by recall."
pharmaRecallCanonicalText = refl
pharmaRecallCompactText
: Explanation.text pharmaRecallCompact
≡ "For every serialized medicine pack pack, every production batch lot, and every market recall recall, if pack belongs to lot and lot is included in recall, then pack is affected by recall."
pharmaRecallCompactText = refl
pharmaRecallEvidenceText
: Explanation.text pharmaRecallEvidence
≡ "For every serialized medicine pack pack, every production batch lot, and every market recall recall, given pack belongs to lot; and lot is included in recall, pack is affected by recall."
pharmaRecallEvidenceText = refl
pharmaRecallStructuredText
: Explanation.text pharmaRecallStructured
≡ "For every serialized medicine pack pack, every production batch lot, and every market recall recall, the following conditions suffice: pack belongs to lot; and lot is included in recall. Under those conditions, pack is affected by recall."
pharmaRecallStructuredText = refl
pharmaRecallDomainText
: Explanation.text pharmaRecallDomain
≡ "For every serialized medicine pack, every production batch, and every market recall, the serialized-pack recall entailment basis in declaration order is: Pack-to-batch traceability — the pack belongs to the batch; and Recall-scope assertion — the batch is included in the recall. Serialized-pack recall consequence — the pack is affected by the recall."
pharmaRecallDomainText = refl
windEnergizationCanonical windEnergizationCompact
windEnergizationEvidence windEnergizationStructured windEnergizationDomain : Explanation
windEnergizationCanonical =
explainName OWLMore.owlMoreDomain
OWLMore.reviewedTurbineEligibleForEnergization
windEnergizationCompact =
explainNameSelected OWLMore.owlMoreDomain "compact/v1"
OWLMore.reviewedTurbineEligibleForEnergization
windEnergizationEvidence =
explainNameSelected OWLMore.owlMoreDomain "evidence/v1"
OWLMore.reviewedTurbineEligibleForEnergization
windEnergizationStructured =
explainNameSelected OWLMore.owlMoreDomain "structured/v1"
OWLMore.reviewedTurbineEligibleForEnergization
windEnergizationDomain =
explainNameDomainEvidence Profiles.windEnergizationProfile
OWLMore.owlMoreDomain OWLMore.reviewedTurbineEligibleForEnergization
windEnergizationCanonicalText
: Explanation.text windEnergizationCanonical
≡ "For every authorized grid engineer engineer, for every offshore wind-turbine asset turbine, if turbine has a current inspection on record, then if turbine has reviewed grid-protection settings, then if engineer is authorized to release turbine, then turbine is eligible for grid energization."
windEnergizationCanonicalText = refl
windEnergizationCompactText
: Explanation.text windEnergizationCompact
≡ "For every authorized grid engineer engineer and every offshore wind-turbine asset turbine, if turbine has a current inspection on record, turbine has reviewed grid-protection settings, and engineer is authorized to release turbine, then turbine is eligible for grid energization."
windEnergizationCompactText = refl
windEnergizationEvidenceText
: Explanation.text windEnergizationEvidence
≡ "For every authorized grid engineer engineer and every offshore wind-turbine asset turbine, given turbine has a current inspection on record; turbine has reviewed grid-protection settings; and engineer is authorized to release turbine, turbine is eligible for grid energization."
windEnergizationEvidenceText = refl
windEnergizationStructuredText
: Explanation.text windEnergizationStructured
≡ "For every authorized grid engineer engineer and every offshore wind-turbine asset turbine, the following conditions suffice: turbine has a current inspection on record; turbine has reviewed grid-protection settings; and engineer is authorized to release turbine. Under those conditions, turbine is eligible for grid energization."
windEnergizationStructuredText = refl
windEnergizationDomainText
: Explanation.text windEnergizationDomain
≡ "For every authorized grid engineer and every offshore wind-turbine asset, the grid-energization release basis in declaration order is: Current inspection evidence — the turbine has a current inspection on record; Grid-protection review — the turbine has reviewed grid-protection settings; and Engineer release authority — the engineer is authorized to release the turbine. Grid-energization disposition — the turbine is eligible for grid energization."
windEnergizationDomainText = refl
motorRestartCanonical motorRestartCompact
motorRestartEvidence motorRestartStructured motorRestartDomain : Explanation
motorRestartCanonical =
explainName Spartan.spartanIndustrialDomain
Spartan.healthyRestartEnergizesBothMotorPermitChannels
motorRestartCompact =
explainNameSelected Spartan.spartanIndustrialDomain "compact/v1"
Spartan.healthyRestartEnergizesBothMotorPermitChannels
motorRestartEvidence =
explainNameSelected Spartan.spartanIndustrialDomain "evidence/v1"
Spartan.healthyRestartEnergizesBothMotorPermitChannels
motorRestartStructured =
explainNameSelected Spartan.spartanIndustrialDomain "structured/v1"
Spartan.healthyRestartEnergizesBothMotorPermitChannels
motorRestartDomain =
explainNameDomainEvidence Profiles.motorPermitProfile
Spartan.spartanIndustrialDomain
Spartan.healthyRestartEnergizesBothMotorPermitChannels
motorRestartCanonicalText
: Explanation.text motorRestartCanonical
≡ "For every recorded motor-control cycle event, if event reports the perimeter guard door closed, then if event reports the emergency-stop safety loop healthy, then if event contains an operator restart command, then if event is a valid rising-edge update of the redundant motor interlock, then event leaves both redundant motor-permit channels energized."
motorRestartCanonicalText = refl
motorRestartCompactText
: Explanation.text motorRestartCompact
≡ "For every recorded motor-control cycle event, if event reports the perimeter guard door closed, event reports the emergency-stop safety loop healthy, event contains an operator restart command, and event is a valid rising-edge update of the redundant motor interlock, then event leaves both redundant motor-permit channels energized."
motorRestartCompactText = refl
motorRestartEvidenceText
: Explanation.text motorRestartEvidence
≡ "For every recorded motor-control cycle event, given event reports the perimeter guard door closed; event reports the emergency-stop safety loop healthy; event contains an operator restart command; and event is a valid rising-edge update of the redundant motor interlock, event leaves both redundant motor-permit channels energized."
motorRestartEvidenceText = refl
motorRestartStructuredText
: Explanation.text motorRestartStructured
≡ "For every recorded motor-control cycle event, the following conditions suffice: event reports the perimeter guard door closed; event reports the emergency-stop safety loop healthy; event contains an operator restart command; and event is a valid rising-edge update of the redundant motor interlock. Under those conditions, event leaves both redundant motor-permit channels energized."
motorRestartStructuredText = refl
motorRestartDomainText
: Explanation.text motorRestartDomain
≡ "For every recorded motor-control cycle, the motor-permit interlock proof basis in declaration order is: Guard interlock input — the recorded cycle reports the perimeter guard door closed; E-stop safety-loop input — the recorded cycle reports the emergency-stop safety loop healthy; Operator restart demand — the recorded cycle contains an operator restart command; and Checked rising-edge transition — the recorded cycle is a valid rising-edge update of the redundant motor interlock. Motor-permit output — the recorded cycle leaves both redundant motor-permit channels energized."
motorRestartDomainText = refl
burnerIgnitionCanonical burnerIgnitionCompact
burnerIgnitionEvidence burnerIgnitionStructured burnerIgnitionDomain : Explanation
burnerIgnitionCanonical =
explainName SpartanMore.spartanMoreDomain
SpartanMore.verifiedPurgeAllowsIgnition
burnerIgnitionCompact =
explainNameSelected SpartanMore.spartanMoreDomain "compact/v1"
SpartanMore.verifiedPurgeAllowsIgnition
burnerIgnitionEvidence =
explainNameSelected SpartanMore.spartanMoreDomain "evidence/v1"
SpartanMore.verifiedPurgeAllowsIgnition
burnerIgnitionStructured =
explainNameSelected SpartanMore.spartanMoreDomain "structured/v1"
SpartanMore.verifiedPurgeAllowsIgnition
burnerIgnitionDomain =
explainNameDomainEvidence Profiles.burnerIgnitionProfile
SpartanMore.spartanMoreDomain SpartanMore.verifiedPurgeAllowsIgnition
burnerIgnitionCanonicalText
: Explanation.text burnerIgnitionCanonical
≡ "For every recorded burner-management sample cycle, if cycle records the purge cycle complete, then if cycle records the furnace proved clear, then if cycle records both automatic fuel valves proved closed, then cycle enables the ignition sequence."
burnerIgnitionCanonicalText = refl
burnerIgnitionCompactText
: Explanation.text burnerIgnitionCompact
≡ "For every recorded burner-management sample cycle, if cycle records the purge cycle complete, cycle records the furnace proved clear, and cycle records both automatic fuel valves proved closed, then cycle enables the ignition sequence."
burnerIgnitionCompactText = refl
burnerIgnitionEvidenceText
: Explanation.text burnerIgnitionEvidence
≡ "For every recorded burner-management sample cycle, given cycle records the purge cycle complete; cycle records the furnace proved clear; and cycle records both automatic fuel valves proved closed, cycle enables the ignition sequence."
burnerIgnitionEvidenceText = refl
burnerIgnitionStructuredText
: Explanation.text burnerIgnitionStructured
≡ "For every recorded burner-management sample cycle, the following conditions suffice: cycle records the purge cycle complete; cycle records the furnace proved clear; and cycle records both automatic fuel valves proved closed. Under those conditions, cycle enables the ignition sequence."
burnerIgnitionStructuredText = refl
burnerIgnitionDomainText
: Explanation.text burnerIgnitionDomain
≡ "For every recorded burner-management sample, the burner ignition-permissive proof basis in declaration order is: Purge completion permissive — the burner sample records the purge cycle complete; Furnace-clear permissive — the burner sample records the furnace proved clear; and Fuel-valve closure proof — the burner sample records both automatic fuel valves proved closed. Ignition-sequence output — the burner sample enables the ignition sequence."
burnerIgnitionDomainText = refl
pumpStartCanonical pumpStartCompact
pumpStartEvidence pumpStartStructured pumpStartDomain : Explanation
pumpStartCanonical =
explainName SpartanMore.spartanMoreDomain
SpartanMore.confirmedDemandPermitsPumpStart
pumpStartCompact =
explainNameSelected SpartanMore.spartanMoreDomain "compact/v1"
SpartanMore.confirmedDemandPermitsPumpStart
pumpStartEvidence =
explainNameSelected SpartanMore.spartanMoreDomain "evidence/v1"
SpartanMore.confirmedDemandPermitsPumpStart
pumpStartStructured =
explainNameSelected SpartanMore.spartanMoreDomain "structured/v1"
SpartanMore.confirmedDemandPermitsPumpStart
pumpStartDomain =
explainNameDomainEvidence Profiles.pumpStartProfile
SpartanMore.spartanMoreDomain SpartanMore.confirmedDemandPermitsPumpStart
pumpStartCanonicalText
: Explanation.text pumpStartCanonical
≡ "For every recorded three-channel pump-demand sample sample, if sample asserts the two-out-of-three high-water demand, then if sample records the drainage-pump drive available, then sample permits the drainage pump start output."
pumpStartCanonicalText = refl
pumpStartCompactText
: Explanation.text pumpStartCompact
≡ "For every recorded three-channel pump-demand sample sample, if sample asserts the two-out-of-three high-water demand and sample records the drainage-pump drive available, then sample permits the drainage pump start output."
pumpStartCompactText = refl
pumpStartEvidenceText
: Explanation.text pumpStartEvidence
≡ "For every recorded three-channel pump-demand sample sample, given sample asserts the two-out-of-three high-water demand; and sample records the drainage-pump drive available, sample permits the drainage pump start output."
pumpStartEvidenceText = refl
pumpStartStructuredText
: Explanation.text pumpStartStructured
≡ "For every recorded three-channel pump-demand sample sample, the following conditions suffice: sample asserts the two-out-of-three high-water demand; and sample records the drainage-pump drive available. Under those conditions, sample permits the drainage pump start output."
pumpStartStructuredText = refl
pumpStartDomainText
: Explanation.text pumpStartDomain
≡ "For every recorded three-channel pump-demand sample, the drainage-pump start-permit proof basis in declaration order is: Two-out-of-three demand vote — the pump-demand sample asserts the two-out-of-three high-water demand; and Pump-drive availability — the pump-demand sample records the drainage-pump drive available. Pump-start output — the pump-demand sample permits the drainage pump start output."
pumpStartDomainText = refl
candidateRuns : List CandidateRun
candidateRuns =
candidate-run "logic" "Batch-reactor discharge"
"pressureVerificationAuthorizesDischarge" "domain-evidence/v1"
(Explanation.text batchReleaseCanonical)
(Explanation.text batchReleaseCompact)
(Explanation.text batchReleaseEvidence)
(Explanation.text batchReleaseStructured)
(Explanation.text batchReleaseDomain)
∷ candidate-run "logic" "Railway movement authority"
"provedBarriersProtectRailMovement" "domain-evidence/v1"
(Explanation.text railProtectionCanonical)
(Explanation.text railProtectionCompact)
(Explanation.text railProtectionEvidence)
(Explanation.text railProtectionStructured)
(Explanation.text railProtectionDomain)
∷ candidate-run "logic" "Cold-chain release"
"reviewedStabilityEvidenceAllowsRelease" "domain-evidence/v1"
(Explanation.text coldReleaseCanonical)
(Explanation.text coldReleaseCompact)
(Explanation.text coldReleaseEvidence)
(Explanation.text coldReleaseStructured)
(Explanation.text coldReleaseDomain)
∷ candidate-run "owl" "Aircraft return to service"
"returnToServiceEligibility" "domain-evidence/v1"
(Explanation.text mroReleaseCanonical)
(Explanation.text mroReleaseCompact)
(Explanation.text mroReleaseEvidence)
(Explanation.text mroReleaseStructured)
(Explanation.text mroReleaseDomain)
∷ candidate-run "owl" "Serialized medicine recall"
"batchRecallPropagatesToPack" "domain-evidence/v1"
(Explanation.text pharmaRecallCanonical)
(Explanation.text pharmaRecallCompact)
(Explanation.text pharmaRecallEvidence)
(Explanation.text pharmaRecallStructured)
(Explanation.text pharmaRecallDomain)
∷ candidate-run "owl" "Offshore wind energization"
"reviewedTurbineEligibleForEnergization" "domain-evidence/v1"
(Explanation.text windEnergizationCanonical)
(Explanation.text windEnergizationCompact)
(Explanation.text windEnergizationEvidence)
(Explanation.text windEnergizationStructured)
(Explanation.text windEnergizationDomain)
∷ candidate-run "spartan" "Motor permit restart"
"healthyRestartEnergizesBothMotorPermitChannels" "domain-evidence/v1"
(Explanation.text motorRestartCanonical)
(Explanation.text motorRestartCompact)
(Explanation.text motorRestartEvidence)
(Explanation.text motorRestartStructured)
(Explanation.text motorRestartDomain)
∷ candidate-run "spartan" "Burner ignition permissive"
"verifiedPurgeAllowsIgnition" "domain-evidence/v1"
(Explanation.text burnerIgnitionCanonical)
(Explanation.text burnerIgnitionCompact)
(Explanation.text burnerIgnitionEvidence)
(Explanation.text burnerIgnitionStructured)
(Explanation.text burnerIgnitionDomain)
∷ candidate-run "spartan" "Pump start permit"
"confirmedDemandPermitsPumpStart" "domain-evidence/v1"
(Explanation.text pumpStartCanonical)
(Explanation.text pumpStartCompact)
(Explanation.text pumpStartEvidence)
(Explanation.text pumpStartStructured)
(Explanation.text pumpStartDomain)
∷ []