emit rows

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

namespace ResourceScheduling.Graph
theorem emit_rows (B N : ℕ) (s : RAMState GraphReg) (hs : RAMBound B s)
    (hn : s.val n = N) (hB : N * N + N ≤ B) (hpos : 1 ≤ B) :
    RAMSafe emitRows B s ∧ (emitRows.eval s).out =
      ((wordNonEdges N s.word).flatMap fun p => (List.range N).flatMap fun k =>
        unary (if k = p.1 ∨ k = p.2 then 1 else 0)).reverse ++ s.out := by sorry
end ResourceScheduling.Graph