let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I, J being parahalting Program of SCM+FSA
for a being read-write Int-Location holds
( if=0 (a,I,J) is parahalting & ( 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 parahalting Program of SCM+FSA
for a being read-write Int-Location holds
( if=0 (a,I,J) is parahalting & ( 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 parahalting Program of SCM+FSA; :: thesis: for a being read-write Int-Location holds
( if=0 (a,I,J) is parahalting & ( 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 parahalting & ( 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)) ) )
A1: I is_halting_on Initialized s,P by SCMFSA7B:25;
A2: ProgramPart (if=0 (a,I,J)) = if=0 (a,I,J) by RELAT_1:209;

now

let s be State of SCM+FSA; :: thesis: ( Initialize (if=0 (a,I,J)) c= s implies for Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT st ProgramPart (Initialize (if=0 (a,I,J))) c= Q holds
b₃ halts_on b₂ )
assume Initialize (if=0 (a,I,J)) c= s ; :: thesis: for Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT st ProgramPart (Initialize (if=0 (a,I,J))) c= Q holds
b₃ halts_on b₂
then A3: s = s +* (Initialize (if=0 (a,I,J))) by FUNCT_4:79;
let Q be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( ProgramPart (Initialize (if=0 (a,I,J))) c= Q implies b₂ halts_on b₁ )
assume A4: ProgramPart (Initialize (if=0 (a,I,J))) c= Q ; :: thesis: b₂ halts_on b₁
A5: if=0 (a,I,J) c= Q by A4, COMPOS_1:144;
A6: I is_closed_on s,Q by SCMFSA7B:24;
A7: I is_halting_on s,Q by SCMFSA7B:25;
A8: J is_halting_on s,Q by SCMFSA7B:25;
A9: J is_closed_on s,Q by SCMFSA7B:24;
A10: Q +* (if=0 (a,I,J)) = Q by A5, FUNCT_4:79;

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_on s,Q by A6, A7, Th16;
hence Q halts_on s by A3, SCMFSA7B:def 8, A2, A10; :: thesis: verum

end;

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

then if=0 (a,I,J) is_halting_on s,Q by A9, A8, Th18;
hence Q halts_on s by A3, SCMFSA7B:def 8, A2, A10; :: thesis: verum

end;

end;

end;

then Initialize (if=0 (a,I,J)) is halting by EXTPRO_1:def 10;
hence if=0 (a,I,J) is parahalting by SCMFSA6B:def 3; :: 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)) ) )
thus ( 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 A1, Th17, SCMFSA7B:24; :: 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_halting_on Initialized s,P by SCMFSA7B:25;
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 Th19, SCMFSA7B:24; :: thesis: verum