for n rule

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

namespace ResourceScheduling.Graph
theorem for_n_rule (counter idx : GraphReg) (hc : n ≠ counter) (hi : idx ≠ n)
    (hic : idx ≠ counter) (p : GraphProgram.Code)
    (hw : p.writes n = false ∧ p.writes idx = false ∧ p.writes counter = false)
    (B N : ℕ) (P : ℕ → RAMState GraphReg → Prop)
    (hpc : ∀ k x a, P k (x.set counter a) ↔ P k x)
    (hpi : ∀ k x a, P k (x.set idx a) ↔ P k x)
    (s : RAMState GraphReg) (hs : RAMBound B s) (hn : s.val n = N) (hp : P 0 s)
    (hstep : ∀ k < N, ∀ x, RAMBound B x → x.val n = N → x.val idx = k → P k x →
      RAMSafe p B x ∧ P (k + 1) (p.eval x)) :
    RAMSafe (GraphProgram.forN counter idx hc p) B s ∧
      ((GraphProgram.forN counter idx hc p).eval s).val idx = N ∧
      ((GraphProgram.forN counter idx hc p).eval s).val counter = 0 ∧
      P N ((GraphProgram.forN counter idx hc p).eval s) := by sorry
end ResourceScheduling.Graph