let s be State of SCM+FSA; :: according to EXTPRO_1:def 10 :: thesis: ( not NPP (Initialized I) c= s or for b₁ being set holds
( not ProgramPart (Initialized I) c= b₁ or b₁ halts_on s ) )
assume A1: NPP (Initialized I) c= s ; :: thesis: for b₁ being set holds
( not ProgramPart (Initialized I) c= b₁ or b₁ halts_on s )
B1: Initialize ((intloc 0) .--> 1) c= s by A1, SCMFSA6A:79;
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart (Initialized I) c= P or P halts_on s )
assume A2: ProgramPart (Initialized I) c= P ; :: thesis: P halts_on s
ProgramPart (Initialized I) = I by SCMFSA6A:33;
hence P halts_on s by A2, Th19, B1; :: thesis: verum