let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I, J being really-closed InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location holds
( IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 & ( s . a = 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & ( s . a <> 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )

let s be State of SCM+FSA; :: thesis: for I, J being really-closed InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location holds
( IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 & ( s . a = 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & ( s . a <> 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )

let I, J be really-closed InitHalting MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location holds
( IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 & ( s . a = 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & ( s . a <> 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )

let a be read-write Int-Location; :: thesis: ( IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 & ( s . a = 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & ( s . a <> 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )
hereby :: thesis: ( ( s . a = 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & ( s . a <> 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )
per cases ( s . a = 0 or s . a <> 0 ) ;
suppose s . a = 0 ; :: thesis: IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3
then IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by Th33;
hence IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 by FUNCT_4:113; :: thesis: verum
end;
suppose s . a <> 0 ; :: thesis: IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3
then IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by Th33;
hence IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 by FUNCT_4:113; :: thesis: verum
end;
end;
end;
hereby :: thesis: ( s . a <> 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) )
assume s . a = 0 ; :: thesis: ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) )
then A1: IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by Th33;
hereby :: thesis: for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f
let d be Int-Location; :: thesis: (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d
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 ; :: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f
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 ; :: thesis: verum
end;
assume s . a <> 0 ; :: thesis: ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) )
then A2: IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by Th33;
hereby :: thesis: for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f
let d be Int-Location; :: thesis: (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d
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 ; :: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f
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 ; :: thesis: verum