prepare eval

import Definitions.Def_ResourceScheduling_Graph_ReductionProgram
open ResourceScheduling.Graph GraphReg GraphProgram

namespace ResourceScheduling.Graph
theorem prepare_eval (s : RAMState GraphReg) :
    (prepare.eval s).val t = (splitOnes s.word).1 ∧
    (prepare.eval s).val n = 3 * (splitOnes s.word).1 ∧
    (prepare.eval s).word = (splitOnes s.word).2.tail ∧
    (prepare.eval s).out = s.out ∧
    (prepare.eval s).val good =
      if (splitOnes s.word).2 ≠ [] ∧ (splitOnes s.word).2.tail.length =
        (3 * (splitOnes s.word).1) * (3 * (splitOnes s.word).1) then 1 else 0 := by sorry
end ResourceScheduling.Graph