@[simp]

instance VerifiedIO.ProgM.wf_pure {α : Type} {x : α} : (pure x).WF

instance VerifiedIO.ProgM.wf_bind {α β : Type} {m : ProgM α} {f : α → ProgM β} [H₁ : m.WF] [H₂ : ∀ (x : α), (f x).WF] : (m >>= f).WF

instance VerifiedIO.ProgM.monadCnd_wf : MonadCnd fun {α : Type} => WF

instance VerifiedIO.ProgM.wf_map {α β : Type} {m : ProgM α} {f : α → β} [H₁ : m.WF] : (f <$> m).WF

@[simp]

instance VerifiedIO.ProgM.wf_ioBit {b : Bit} : (ioBit b).WF

@[simp]

instance VerifiedIO.Prog.wf_toProgM {p : Prog} : p.toProgM.WF

@[simp]

theorem VerifiedIO.toProg_toProgM {p : Prog} : p.toProgM.toProg = p

theorem VerifiedIO.toProgM_toProg {m : ProgM Unit} (h : ∀ (bs : List Bit), ∃ (b : Bit), StateT.run m bs = Sum.inl b) : m.toProg.toProgM = m

@[simp]

theorem VerifiedIO.run_ioBit_nil {b : Bit} : StateT.run (ioBit b) [] = Sum.inl b

@[simp]

theorem VerifiedIO.run_ioBit_cons {b b₁ : Bit} {bs : List Bit} : StateT.run (ioBit b) (b₁ :: bs) = Sum.inr (b₁, bs)

@[simp]

theorem VerifiedIO.run_readBit_nil : StateT.run readBit [] = Sum.inl 0

@[simp]

theorem VerifiedIO.run_readBit_cons {b : Bit} {bs : List Bit} : StateT.run readBit (b :: bs) = Sum.inr (b, bs)

@[simp]

theorem VerifiedIO.run_writeBit_nil {b : Bit} : StateT.run (writeBit b) [] = Sum.inl b

@[simp]

theorem VerifiedIO.run_writeBit_cons {b b₁ : Bit} {bs : List Bit} : StateT.run (writeBit b) (b₁ :: bs) = Sum.inr ((), bs)

@[simp]

instance VerifiedIO.ProgM.wf_readBit : readBit.WF

@[simp]

instance VerifiedIO.ProgM.wf_writeBit {b : Bit} : (writeBit b).WF

@[simp]

instance VerifiedIO.ProgM.wf_readBitsUntil {p : List Bit → Bool} : (readBitsUntil p).WF

@[simp]

instance VerifiedIO.ProgM.wf_readNat : readNat.WF

@[simp]

instance VerifiedIO.ProgM.wf_writeNat {n : ℕ} : (writeNat n).WF