let p be Instruction-Sequence of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
let I, J be really-closed InitHalting MacroInstruction 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)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by Th39;
hence IC (IExec ((if>0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 by FUNCT_4:113; :: thesis:

end;

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

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

end;

end;

end;

hereby :: thesis:

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

hereby :: thesis:

let d be Int-Location; :: thesis:
not d in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by SCMFSA_2:102;
hence (IExec ((if>0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d by A1, FUNCT_4:11; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
not f in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by SCMFSA_2:103;
hence (IExec ((if>0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f by A1, FUNCT_4:11; :: thesis:

end;

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

hereby :: thesis:

let d be Int-Location; :: thesis:
not d in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by SCMFSA_2:102;
hence (IExec ((if>0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d by A2, FUNCT_4:11; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
not f in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by SCMFSA_2:103;
hence (IExec ((if>0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f by A2, FUNCT_4:11; :: thesis: