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