let a be Int_position ; :: thesis: for s being State of
for loc being Instruction-Location of SCMPDS holds
( IC (Initialized s) = inspos 0 & (Initialized s) . a = s . a & (Initialized s) . loc = s . loc )
let s be State of ; :: thesis: for loc being Instruction-Location of SCMPDS holds
( IC (Initialized s) = inspos 0 & (Initialized s) . a = s . a & (Initialized s) . loc = s . loc )
let loc be Instruction-Location of SCMPDS ; :: thesis: ( IC (Initialized s) = inspos 0 & (Initialized s) . a = s . a & (Initialized s) . loc = s . loc )
dom (Start-At (inspos 0 )) = {(IC SCMPDS )} by FUNCOP_1:19;
then A1: IC SCMPDS in dom (Start-At (inspos 0 )) by TARSKI:def 1;
(Start-At (inspos 0 )) . (IC SCMPDS ) = inspos 0 by FUNCOP_1:87;
hence IC (Initialized s) = inspos 0 by A1, FUNCT_4:14; :: thesis: ( (Initialized s) . a = s . a & (Initialized s) . loc = s . loc )
not a in dom (Start-At (inspos 0 )) by SCMPDS_4:59;
hence (Initialized s) . a = s . a by FUNCT_4:12; :: thesis: (Initialized s) . loc = s . loc
not loc in dom (Start-At (inspos 0 )) by AMI_1:137;
hence (Initialized s) . loc = s . loc by FUNCT_4:12; :: thesis: verum