module SMT.Unsafe.SystemsAssume where

open import Cubical.Foundations.Prelude

open import SMT.Core using (Statement)
open import SMT.Examples.Systems
open import SMT.Unsafe.Z3

queue-step-preserves-bounds-type : Type₀
queue-step-preserves-bounds-type =
  z3CheckedStatement valid-queue-step-preserves-bounds

queue-step-preserves-bounds-type-ok :
  queue-step-preserves-bounds-type ≡ Statement valid-queue-step-preserves-bounds
queue-step-preserves-bounds-type-ok = refl

scheduled-tasks-type : Type₀
scheduled-tasks-type =
  z3CheckedStatement valid-scheduled-tasks-are-nonoverlapping-and-finish

scheduled-tasks-type-ok :
  scheduled-tasks-type ≡
  Statement valid-scheduled-tasks-are-nonoverlapping-and-finish
scheduled-tasks-type-ok = refl

quorum-three-type : Type₀
quorum-three-type =
  z3CheckedStatement valid-quorum-three-gives-pairwise-coverage

quorum-three-type-ok :
  quorum-three-type ≡ Statement valid-quorum-three-gives-pairwise-coverage
quorum-three-type-ok = refl