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 Z1: NPP (Initialized I) c= s ; :: thesis: for b₁ being set holds
( not ProgramPart (Initialized I) c= b₁ or b₁ halts_on s )
U2: NPP (Initialized I) c= s by Z1;
U1: NPP (Initialized I) = Initialize ((intloc 0) .--> 1) by SCMFSA6A:79;
XX: ProgramPart (Initialized I) = I by SCMFSA6A:33;
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 Z2: ProgramPart (Initialized I) c= P ; :: thesis: P halts_on s
thus P halts_on s by Z2, Def2, U1, U2, XX; :: thesis: verum