set I = goto 0 ;
let s be State of SCMPDS ; :: according to AMI_1:def 8 :: thesis: Exec (goto 0 ),s = s
reconsider S = s as SCMPDS-State by PBOOLE:155;
reconsider Es = Exec (goto 0 ),s as SCMPDS-State by PBOOLE:155;
A1: dom Es = the carrier of SCMPDS by PARTFUN1:def 4
.= 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 4;

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

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

reconsider n = IC s as Element of NAT ;
consider k being Element of NAT such that
A5: n = k ;
A6: 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 A4, A5, Th6, Th66
.= k by A5, A6, ABSVALUE:def 1
.= S . x by A4, A5, 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;

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

then reconsider v = x as Element of NAT ;
reconsider I0 = goto 0 as Element of SCMPDS-Instr ;
Exec (goto 0 ),s = SCM-Exec-Res I0,S by SCMPDS_1:def 25
.= SCM-Chg S,(jump_address S,(I0 const_INT )) by SCMPDS_1:def 24 ;
hence Es . x = S . v by SCMPDS_1:28
.= S . x ;
:: thesis: verum

end;

end;

end;

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