block laws

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

namespace ResourceScheduling.Graph
theorem block_laws (ps qs : List Code) (B : ℕ) (s : RAMState GraphReg) :
    (block (ps ++ qs)).eval s = (block qs).eval ((block ps).eval s) ∧
    (RAMSafe (block ps) B s → RAMSafe (block qs) B ((block ps).eval s) →
      RAMSafe (block (ps ++ qs)) B s) := by sorry
end ResourceScheduling.Graph