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 holds
( Initialized I is_halting_on s,P iff I is_halting_on Initialized s,P )
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds
( Initialized I is_halting_on s,P iff I is_halting_on Initialized s,P )
let I be Program of SCM+FSA; :: thesis: ( Initialized I is_halting_on s,P iff I is_halting_on Initialized s,P )
A1: ProgramPart I = I by RELAT_1:209;
A2: ProgramPart (Initialized I) = I by SCMFSA6A:33;
A3: s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I) by Th16;

hereby :: thesis: ( I is_halting_on Initialized s,P implies Initialized I is_halting_on s,P )

assume Initialized I is_halting_on s,P ; :: thesis: I is_halting_on Initialized s,P
then P +* I halts_on s +* (Initialize (Initialized I)) by SCMFSA7B:def 8, A2;
then P +* I halts_on (Initialized s) +* (Initialize I) by A3;
hence I is_halting_on Initialized s,P by SCMFSA7B:def 8, A1; :: thesis: verum

end;

assume I is_halting_on Initialized s,P ; :: thesis: Initialized I is_halting_on s,P
then P +* I halts_on (Initialized s) +* (Initialize I) by SCMFSA7B:def 8, A1;
then P +* I halts_on s +* (Initialize (Initialized I)) by A3;
hence Initialized I is_halting_on s,P by SCMFSA7B:def 8, A2; :: thesis: verum