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 (insloc (((card I) + (card J)) + 3))) ) & ( s . a <= 0 implies IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )
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 (insloc (((card I) + (card J)) + 3))) ) & ( s . a <= 0 implies IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )
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 (insloc (((card I) + (card J)) + 3))) ) & ( s . a <= 0 implies IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )

now

let s be State of SCM+FSA ; :: thesis: ( Initialized (if>0 a,I,J) c= s implies b₁ is halting )
assume Initialized (if>0 a,I,J) c= s ; :: thesis: b₁ is halting
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: b₁ is halting

then if>0 a,I,J is_halting_onInit s by A3, Th49;
hence s is halting by A1, Def5; :: thesis: verum

end;

suppose s . a <= 0 ; :: thesis: b₁ is halting

then if>0 a,I,J is_halting_onInit s by A2, Th51;
hence s is halting by A1, Def5; :: thesis: verum

end;

end;

end;

then Initialized (if>0 a,I,J) is halting by AMI_1:def 26;
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 (insloc (((card I) + (card J)) + 3))) ) & ( s . a <= 0 implies IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )
( 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 (insloc (((card I) + (card J)) + 3))) ) by Th50; :: thesis: ( s . a <= 0 implies IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) )
( 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 (insloc (((card I) + (card J)) + 3))) ) by Th52; :: thesis: verum