let k be Integer; :: thesis: for loc being Instruction-Location of SCMPDS ex s being State of SCMPDS st
( s . NAT = loc & ( for d being Int_position holds s . d = k ) )
let loc be Instruction-Location of SCMPDS ; :: thesis: ex s being State of SCMPDS st
( s . NAT = loc & ( for d being Int_position holds s . d = k ) )
consider s1 being State of SCMPDS such that
A1: for d being Int_position holds s1 . d = k by Th73;
reconsider S = s1 as SCMPDS-State ;
set t = S +* (NAT .--> loc);
set f = the Object-Kind of SCMPDS ;
A2: dom (NAT .--> loc) = {NAT } by FUNCOP_1:19;
then NAT in dom (NAT .--> loc) by TARSKI:def 1;
then A3: (S +* (NAT .--> loc)) . NAT = (NAT .--> loc) . NAT by FUNCT_4:14
.= loc by FUNCOP_1:87 ;
then A4: (S +* (NAT .--> loc)) . NAT in NAT by AMI_1:def 4;
A5: {NAT } c= SCM-Memory by AMI_2:30, ZFMISC_1:37;
A6: dom S = dom SCMPDS-OK by CARD_3:18;
A7: dom (S +* (NAT .--> loc)) = (dom S) \/ (dom (NAT .--> loc)) by FUNCT_4:def 1
.= SCM-Memory \/ (dom (NAT .--> loc)) by A6, FUNCT_2:def 1
.= SCM-Memory \/ {NAT } by FUNCOP_1:19
.= SCM-Memory by A5, XBOOLE_1:12 ;
A8: dom the Object-Kind of SCMPDS = SCM-Memory by FUNCT_2:def 1;
for x being set st x in dom the Object-Kind of SCMPDS holds
(S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x

proof

let x be set ; :: thesis: ( x in dom the Object-Kind of SCMPDS implies (S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x )
assume A9: x in dom the Object-Kind of SCMPDS ; :: thesis: (S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x

per cases ( x = NAT or x <> NAT ) ;

suppose A10: x = NAT ; :: thesis: (S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x

thus (S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x by A4, A10, AMI_2:30, SCMPDS_1:18; :: thesis: verum

end;

suppose x <> NAT ; :: thesis: (S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x

then not x in dom (NAT .--> loc) by A2, TARSKI:def 1;
then (S +* (NAT .--> loc)) . x = S . x by FUNCT_4:12;
hence (S +* (NAT .--> loc)) . x in the Object-Kind of SCMPDS . x by A9, CARD_3:18; :: thesis: verum

end;

end;

end;

then reconsider s = S +* (NAT .--> loc) as State of SCMPDS by A7, A8, CARD_3:18;
take s ; :: thesis: ( s . NAT = loc & ( for d being Int_position holds s . d = k ) )
thus s . NAT = loc by A3; :: thesis: for d being Int_position holds s . d = k

hereby :: thesis: verum

let d be Int_position ; :: thesis: s . d = k
d in SCM-Data-Loc by Def2;
then consider j being Element of NAT such that
A11: d = [1,j] by AMI_2:32;

now

assume d in dom (NAT .--> loc) ; :: thesis: contradiction
then d = NAT by A2, TARSKI:def 1;
hence contradiction by A11, ARYTM_3:36; :: thesis: verum

end;

hence s . d = s1 . d by FUNCT_4:12
.= k by A1 ;
:: thesis: verum

end;