simp [GSN_IA', GSN_IA]
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (GSN_IA' S S' A R D | ρ) = GSN_IA (S | ρ) (S' | ρ) (A | ρ) (R | ρ) (D | ρ)
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys (S | ρ) ((D | ρ).delete ∪ (D | ρ).modify)) ∪
            trace (restrict (R | ρ) (D | ρ)) (sliceSys (S' | ρ) ((D | ρ).add ∪ (D | ρ).modify)) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D | ρ).delete)))
      (trace (R | ρ) (D | ρ).delete)