set I = goto 0;
let s be State of SCMPDS; :: according to EXTPRO_1:def 3 :: thesis: Exec ((goto 0),s) = s
reconsider S = s as SCMPDS-State by CARD_3:107;
reconsider Es = Exec ((goto 0),s) as SCMPDS-State by CARD_3:107;
A1: dom Es = the carrier of SCMPDS by PARTFUN1:def 2
.= SCM-Memory ;

A2: now

let x be set ; :: thesis: ( x in dom s implies Es . b₁ = S . b₁ )
assume x in dom s ; :: thesis: Es . b₁ = S . b₁
then reconsider m = x as Element of SCM-Memory by PARTFUN1:def 2;

per cases ( m = NAT or m in SCM-Data-Loc ) by SCMPDS_1:5;

suppose A3: m = NAT ; :: thesis: Es . b₁ = S . b₁

reconsider n = IC s as Element of NAT ;
consider k being Element of NAT such that
A4: n = k ;
A5: n >= 0 by NAT_1:2;
ex m being Element of NAT st
( m = IC s & ICplusConst (s,0) = abs (m + (2 * 0)) ) by Def20;
hence Es . x = abs (0 + k) by A3, A4, Th6, Th66
.= k by A4, A5, ABSVALUE:def 1
.= S . x by A3, A4, FUNCT_7:def 1 ;
:: thesis: verum

end;

suppose m in SCM-Data-Loc ; :: thesis: Es . b₁ = S . b₁

then reconsider d = x as Int_position by Def2;
thus Es . x = s . d by Th66
.= S . x ; :: thesis: verum

end;

end;

end;

dom S = the carrier of SCMPDS by PARTFUN1:def 2
.= SCM-Memory ;
hence Exec ((goto 0),s) = s by A2, A1, FUNCT_1:2; :: thesis: verum