cells eval

import Definitions.Def_ResourceScheduling_Graph_ReductionProgram
open ResourceScheduling.Graph GraphReg

namespace ResourceScheduling.Graph
theorem cells_eval (s : RAMState GraphReg) :
    (GraphProgram.validateCell.eval s).val good =
      (if s.word.getD (s.val i * s.val n + s.val j) Letter.sep = Letter.one ∧
        s.word.getD (s.val j * s.val n + s.val i) Letter.sep ≠ Letter.one then 0 else s.val good) ∧
    ((GraphProgram.ifNonEdge (.inc count)).eval s).val count = s.val count +
      (if s.val i < s.val j ∧ s.word.getD (s.val i * s.val n + s.val j) Letter.sep ≠ Letter.one
        then 1 else 0) ∧
    (GraphProgram.emitCell.eval s).out =
      (unary (if s.val k = s.val i ∨ s.val k = s.val j then 1 else 0)).reverse ++ s.out := by sorry
end ResourceScheduling.Graph