let s be State of SCM+FSA; :: thesis: for i being Instruction of SCM+FSA st InsCode i in {0,6,7,8} holds
DataPart (Exec (i,s)) = DataPart s
let i be Instruction of SCM+FSA; :: thesis: ( InsCode i in {0,6,7,8} implies DataPart (Exec (i,s)) = DataPart s )
assume A1: InsCode i in {0,6,7,8} ; :: thesis: DataPart (Exec (i,s)) = DataPart s
now :: thesis: for a being Int-Location
for f being FinSeq-Location holds
( (Exec (i,s)) . a = s . a & (Exec (i,s)) . f = s . f )
let a be Int-Location; :: thesis: for f being FinSeq-Location holds
( (Exec (i,s)) . b2 = s . b2 & (Exec (i,s)) . b3 = s . b3 )
let f be FinSeq-Location ; :: thesis: ( (Exec (i,s)) . b1 = s . b1 & (Exec (i,s)) . b2 = s . b2 )
per cases ( InsCode i = 0 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by A1, ENUMSET1:def 2;
suppose InsCode i = 0 ; :: thesis: ( (Exec (i,s)) . b1 = s . b1 & (Exec (i,s)) . b2 = s . b2 )
then i = halt SCM+FSA by SCMFSA_2:95;
hence ( (Exec (i,s)) . a = s . a & (Exec (i,s)) . f = s . f ) by EXTPRO_1:def 3; :: thesis: verum
end;
suppose InsCode i = 6 ; :: thesis: ( (Exec (i,s)) . b1 = s . b1 & (Exec (i,s)) . b2 = s . b2 )
then ex lb being Nat st i = goto lb by SCMFSA_2:35;
hence ( (Exec (i,s)) . a = s . a & (Exec (i,s)) . f = s . f ) by SCMFSA_2:69; :: thesis: verum
end;
suppose InsCode i = 7 ; :: thesis: ( (Exec (i,s)) . b1 = s . b1 & (Exec (i,s)) . b2 = s . b2 )
then ex lb being Nat ex b being Int-Location st i = b =0_goto lb by SCMFSA_2:36;
hence ( (Exec (i,s)) . a = s . a & (Exec (i,s)) . f = s . f ) by SCMFSA_2:70; :: thesis: verum
end;
suppose InsCode i = 8 ; :: thesis: ( (Exec (i,s)) . b1 = s . b1 & (Exec (i,s)) . b2 = s . b2 )
then ex lb being Nat ex b being Int-Location st i = b >0_goto lb by SCMFSA_2:37;
hence ( (Exec (i,s)) . a = s . a & (Exec (i,s)) . f = s . f ) by SCMFSA_2:71; :: thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s)) = DataPart s by SCMFSA_M:2; :: thesis: verum