emit pair

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

namespace ResourceScheduling.Graph
theorem emit_pair (B N : ℕ) (s : RAMState GraphReg) (hs : RAMBound B s)
    (hi : s.val i ≤ N) (hj : s.val j ≤ N) (hn : s.val n = N)
    (hB : N * N + N ≤ B) (hpos : 1 ≤ B) :
    RAMSafe (ifNonEdge (forN c2 k (by decide) emitCell)) B s ∧
    ((ifNonEdge (forN c2 k (by decide) emitCell)).eval s).out =
      (if s.val i < s.val j ∧ s.word.getD (s.val i * N + s.val j) Letter.sep ≠ Letter.one
        then ((List.range N).flatMap fun k => unary (if k = s.val i ∨ k = s.val j then 1 else 0))
        else []).reverse ++ s.out := by sorry
end ResourceScheduling.Graph