let p be Instruction-Sequence of SCM+FSA; 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; 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 ; 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; ( 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 ( ( 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
;
IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3then
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;
verum end; suppose
s . a <> 0
;
IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3then
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;
verum end; end;
end;
hereby ( 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
;
( ( 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 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;
(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 A1, FUNCT_4:11;
verum
end; let f be
FinSeq-Location ;
(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 A1, FUNCT_4:11;
verum
end;
assume
s . a <> 0
; ( ( 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 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;
(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 A2, FUNCT_4:11;
verum
end;
let f be FinSeq-Location ; (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 A2, FUNCT_4:11; verum