let P be Instruction-Sequence of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
let I, J be really-closed parahalting 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 Th11;
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 Th11;
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 Th11;

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 Th11;

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: