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:

suppose s . a = 0 ; :: thesis:

then IExec ((if=0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by Th20;
hence IC (IExec ((if=0 (a,I,J)),s)) = ((card I) + (card J)) + 3 by FUNCT_4:121; :: thesis:

end;

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

then IExec ((if=0 (a,I,J)),s) = (IExec (J,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by Th20;
hence IC (IExec ((if=0 (a,I,J)),s)) = ((card I) + (card J)) + 3 by FUNCT_4:121; :: thesis:

end;

end;

end;

hereby :: thesis:

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

hereby :: thesis:

let d be Int-Location ; :: thesis:
not d in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) 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 ((((card I) + (card J)) + 3),SCM+FSA)) 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 ((((card I) + (card J)) + 3),SCM+FSA)) by Th20;

hereby :: thesis:

let d be Int-Location ; :: thesis:
not d in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) 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 ((((card I) + (card J)) + 3),SCM+FSA)) by SCMFSA6B:10;
hence (IExec ((if=0 (a,I,J)),s)) . f = (IExec (J,s)) . f by A2, FUNCT_4:12; :: thesis: