let s be State of SCM+FSA ; :: thesis:
let I, J be parahalting Program of SCM+FSA ; :: thesis:
let a be read-write Int-Location ; :: thesis:

hereby :: thesis:

per cases ;

suppose s . a = 0 ; :: thesis:

then IExec (if=0 a,I,J),s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) by Th20;
hence IC (IExec (if=0 a,I,J),s) = insloc (((card I) + (card J)) + 3) by AMI_1:111; :: thesis:

end;

suppose s . a <> 0 ; :: thesis:

then IExec (if=0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) by Th20;
hence IC (IExec (if=0 a,I,J),s) = insloc (((card I) + (card J)) + 3) by AMI_1:111; :: thesis:

end;

hereby :: thesis:

assume s . a = 0 ; :: thesis:
then A1: IExec (if=0 a,I,J),s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) by Th20;

hereby :: thesis:

let d be Int-Location ; :: thesis:
not d in dom (Start-At (insloc (((card I) + (card J)) + 3))) by SCMFSA6B:9;
hence (IExec (if=0 a,I,J),s) . d = (IExec I,s) . d by A1, FUNCT_4:12; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
not f in dom (Start-At (insloc (((card I) + (card J)) + 3))) by SCMFSA6B:10;
hence (IExec (if=0 a,I,J),s) . f = (IExec I,s) . f by A1, FUNCT_4:12; :: thesis:

end;

assume s . a <> 0 ; :: thesis:
then A2: IExec (if=0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) by Th20;

hereby :: thesis:

let d be Int-Location ; :: thesis:
not d in dom (Start-At (insloc (((card I) + (card J)) + 3))) by SCMFSA6B:9;
hence (IExec (if=0 a,I,J),s) . d = (IExec J,s) . d by A2, FUNCT_4:12; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
not f in dom (Start-At (insloc (((card I) + (card J)) + 3))) by SCMFSA6B:10;
hence (IExec (if=0 a,I,J),s) . f = (IExec J,s) . f by A2, FUNCT_4:12; :: thesis: