emit program

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

namespace ResourceScheduling.Graph
theorem emit_program (B : ℕ) (s : RAMState GraphReg) (hs : RAMBound B s)
    (hn : s.val n = 3 * s.val t) (hc : s.val count = (wordNonEdges (s.val n) s.word).length)
    (hB : s.val n * s.val n + s.val n ≤ B) (hpos : 2 ≤ B) :
    RAMSafe emit B s ∧ (emit.eval s).out = (emitQ2Word (s.val t) s.word).reverse ++ s.out := by sorry
end ResourceScheduling.Graph