let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
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)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <= 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
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)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <= 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,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)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <= 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,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)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <= 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )

now

let s be State of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT st if>0 (a,I,J) c= p holds
b₃ halts_on b₂ )
assume Initialize ((intloc 0) .--> 1) c= s ; :: thesis: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT st if>0 (a,I,J) c= p holds
b₃ halts_on b₂
then A2: s = s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:103, FUNCT_4:104;
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( if>0 (a,I,J) c= p implies b₂ halts_on b₁ )
assume if>0 (a,I,J) c= p ; :: thesis: b₂ halts_on b₁
then A3: p = p +* (if>0 (a,I,J)) by FUNCT_4:103, FUNCT_4:104;
A4: ( J is_closed_onInit s,p & J is_halting_onInit s,p ) by Th35, Th36;
A5: ( I is_closed_onInit s,p & I is_halting_onInit s,p ) by Th35, Th36;

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

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

then if>0 (a,I,J) is_halting_onInit s,p by A5, Th49;
hence p halts_on s by A2, Def5, A3; :: thesis: verum

end;

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

then if>0 (a,I,J) is_halting_onInit s,p by A4, Th51;
hence p halts_on s by A2, Def5, A3; :: thesis: verum

end;

end;

end;

hence if>0 (a,I,J) is InitHalting by Def2; :: thesis: ( ( s . a > 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <= 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
( I is_closed_onInit s,p & I is_halting_onInit s,p ) by Th35, Th36;
hence ( s . a > 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) by Th50; :: thesis: ( s . a <= 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
( J is_closed_onInit s,p & J is_halting_onInit s,p ) by Th35, Th36;
hence ( s . a <= 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) by Th52; :: thesis: verum