emit header

import Definitions.Def_ResourceScheduling_Graph_ReductionProgram
import Definitions.Def_ResourceScheduling_Graph_RAMSafe
open ResourceScheduling.Graph GraphReg GraphProgram

namespace ResourceScheduling.Graph
theorem emit_header (B : ℕ) (s : RAMState GraphReg) (hs : RAMBound B s) (hB : 2 ≤ B) :
    let p := block [.zero num, .inc num, .inc num, .emit num,
      .zero num, .inc num, .emit num, .emit n, .emit count]
    RAMSafe p B s ∧ p.eval s =
      { s.set num 1 with out :=
        (unary 2 ++ unary 1 ++ unary (s.val n) ++ unary (s.val count)).reverse ++ s.out } := by sorry
end ResourceScheduling.Graph