let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0) = 1 holds
( I is_pseudo-closed_on s,P iff I is_pseudo-closed_on Initialized s,P )
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st s . (intloc 0) = 1 holds
( I is_pseudo-closed_on s,P iff I is_pseudo-closed_on Initialized s,P )
set D = Data-Locations SCM+FSA;
let I be Program of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 implies ( I is_pseudo-closed_on s,P iff I is_pseudo-closed_on Initialized s,P ) )
assume s . (intloc 0) = 1 ; :: thesis: ( I is_pseudo-closed_on s,P iff I is_pseudo-closed_on Initialized s,P )
then DataPart s = DataPart (Initialized s) by Th27;
hence ( I is_pseudo-closed_on s,P iff I is_pseudo-closed_on Initialized s,P ) by Th52; :: thesis: verum