non edge safe

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

namespace ResourceScheduling.Graph
theorem non_edge_safe (p : Code) (B N : ℕ) (P : RAMState GraphReg → Prop)
    (hP : ∀ v ∈ [delta, index, bitA], ∀ s x, P s → P (s.set v x))
    (hp : ∀ s, RAMBound B s → P s → RAMSafe p B s)
    (s : RAMState GraphReg) (hs : RAMBound B s) (hPs : P 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 p) B s := by sorry
end ResourceScheduling.Graph