let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for l being Element of NAT holds
( I is_closed_on s,P iff I is_closed_on s +* (Start-At (0,SCM+FSA)),P +* I )
let s be State of SCM+FSA; :: thesis: for I, J being Program of SCM+FSA
for l being Element of NAT holds
( I is_closed_on s,P iff I is_closed_on s +* (Start-At (0,SCM+FSA)),P +* I )
let I, J be Program of SCM+FSA; :: thesis: for l being Element of NAT holds
( I is_closed_on s,P iff I is_closed_on s +* (Start-At (0,SCM+FSA)),P +* I )
let l be Element of NAT ; :: thesis: ( I is_closed_on s,P iff I is_closed_on s +* (Start-At (0,SCM+FSA)),P +* I )
DataPart s = DataPart (Initialize s) by MEMSTR_0:79;
hence ( I is_closed_on s,P iff I is_closed_on s +* (Start-At (0,SCM+FSA)),P +* I ) by Th6; :: thesis: verum