let s be State of SCM+FSA; :: thesis: for I, J being InitHalting Program of SCM+FSA
for a being read-write Int-Location holds
( if=0 (a,I,J) is InitHalting & ( s . a = 0 implies IExec ((if=0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
let I, J be InitHalting Program of SCM+FSA; :: thesis: for a being read-write Int-Location holds
( if=0 (a,I,J) is InitHalting & ( s . a = 0 implies IExec ((if=0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
let a be read-write Int-Location ; :: thesis: ( if=0 (a,I,J) is InitHalting & ( s . a = 0 implies IExec ((if=0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )

now

let s be State of SCM+FSA; :: thesis: ( Initialized (if=0 (a,I,J)) c= s implies ProgramPart b₁ halts_on b₁ )
assume Initialized (if=0 (a,I,J)) c= s ; :: thesis: ProgramPart b₁ halts_on b₁
then A1: s = s +* (Initialized (if=0 (a,I,J))) by FUNCT_4:79;
A2: ( J is_closed_onInit s & J is_halting_onInit s ) by Th35, Th36;
A3: ( I is_closed_onInit s & I is_halting_onInit s ) by Th35, Th36;

per cases ( s . a = 0 or s . a <> 0 ) ;

suppose s . a = 0 ; :: thesis: ProgramPart b₁ halts_on b₁

then if=0 (a,I,J) is_halting_onInit s by A3, Th43;
hence ProgramPart s halts_on s by A1, Def5; :: thesis: verum

end;

suppose s . a <> 0 ; :: thesis: ProgramPart b₁ halts_on b₁

then if=0 (a,I,J) is_halting_onInit s by A2, Th45;
hence ProgramPart s halts_on s by A1, Def5; :: thesis: verum

end;

end;

end;

then Initialized (if=0 (a,I,J)) is halting by EXTPRO_1:def 10;
hence if=0 (a,I,J) is InitHalting by Def2; :: thesis: ( ( s . a = 0 implies IExec ((if=0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
( I is_closed_onInit s & I is_halting_onInit s ) by Th35, Th36;
hence ( s . a = 0 implies IExec ((if=0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) by Th44; :: thesis: ( s . a <> 0 implies IExec ((if=0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
( J is_closed_onInit s & J is_halting_onInit s ) by Th35, Th36;
hence ( s . a <> 0 implies IExec ((if=0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) by Th46; :: thesis: verum