let s be State of SCM+FSA ; :: thesis: for I, J being Program of SCM+FSA
for l being Instruction-Location of SCM+FSA holds
( I is_closed_on s & I is_halting_on s iff ( I is_closed_on s +* (I +* (Start-At l)) & I is_halting_on s +* (I +* (Start-At l)) ) )
let I, J be Program of SCM+FSA ; :: thesis: for l being Instruction-Location of SCM+FSA holds
( I is_closed_on s & I is_halting_on s iff ( I is_closed_on s +* (I +* (Start-At l)) & I is_halting_on s +* (I +* (Start-At l)) ) )
let l be Instruction-Location of SCM+FSA ; :: thesis: ( I is_closed_on s & I is_halting_on s iff ( I is_closed_on s +* (I +* (Start-At l)) & I is_halting_on s +* (I +* (Start-At l)) ) )
DataPart s = DataPart (s +* (I +* (Start-At l))) by SCMFSA8A:11;
hence ( I is_closed_on s & I is_halting_on s iff ( I is_closed_on s +* (I +* (Start-At l)) & I is_halting_on s +* (I +* (Start-At l)) ) ) by Th8; :: thesis: verum