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 ) ) ) )

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;

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: verum

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 ) ) ) )
end;

per cases
( s . a = 0 or s . a <> 0 )
;

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 (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;hence IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 by FUNCT_4:113; :: thesis: verum

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;hence IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 by FUNCT_4:113; :: thesis: verum

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

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: verum

end;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 f be FinSeq-Location ; :: thesis: (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . flet 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 A1, FUNCT_4:11; :: thesis: verum

end;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: verum

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: verum

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 f be FinSeq-Location ; :: thesis: (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . flet 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 A2, FUNCT_4:11; :: thesis: verum

end;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: verum

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: verum