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),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 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),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 parahalting & ( 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 ) ) )
A1: I is_halting_on Initialized s by SCMFSA7B:25;

now

let s be State of SCM+FSA ; :: thesis: ( (if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ) c= s implies ProgramPart b₁ halts_on b₁ )
A2: I is_closed_on s by SCMFSA7B:24;
A3: I is_halting_on s by SCMFSA7B:25;
A4: J is_halting_on s by SCMFSA7B:25;
A5: J is_closed_on s by SCMFSA7B:24;
assume (if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ) c= s ; :: thesis: ProgramPart b₁ halts_on b₁
then A6: s = s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:79;

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

end;

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

then if=0 a,I,J is_halting_on s by A5, A4, Th18;
hence ProgramPart s halts_on s by A6, SCMFSA7B:def 8; :: thesis: verum

end;

end;

end;

then (if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ) is halting by AMI_1:def 26;
hence if=0 a,I,J is parahalting by SCMFSA6B:def 3; :: 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_on Initialized s by SCMFSA7B:24;
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 A1, Th17; :: thesis: ( s . a <> 0 implies IExec (if=0 a,I,J),s = (IExec J,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) )
A7: J is_halting_on Initialized s by SCMFSA7B:25;
J is_closed_on Initialized s by SCMFSA7B:24;
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 A7, Th19; :: thesis: verum