deffunc H₁( Element of NAT ) -> Element of the Instructions of SCMPDS = goto 0 ;
deffunc H₂( Element of NAT ) -> set = t . (DataLoc $1,0 );
consider s being State of SCMPDS such that
A1: ( IC s = inspos 0 & ( for i being Element of NAT holds
( s . (inspos i) = H₁(i) & s . (DataLoc i,0 ) = H₂(i) ) ) ) from SCMPDS_4:sch 1();
take s ; :: thesis: for x being set holds
( ( x in SCM-Data-Loc implies s . x = t . x ) & ( x in NAT implies s . x = goto 0 ) & ( x = IC SCMPDS implies s . x = inspos 0 ) )

now

let x be set ; :: thesis: ( ( x in SCM-Data-Loc implies s . x = t . x ) & ( x in NAT implies s . x = goto 0 ) & ( x = IC SCMPDS implies s . x = inspos 0 ) )
thus ( x in SCM-Data-Loc implies s . x = t . x ) :: thesis: ( ( x in NAT implies s . x = goto 0 ) & ( x = IC SCMPDS implies s . x = inspos 0 ) )

proof

assume x in SCM-Data-Loc ; :: thesis: s . x = t . x
then x is Int_position by SCMPDS_2:9;
then consider i being Element of NAT such that
A2: x = intpos i by Th1;
x = intpos (i + 0 ) by A2
.= DataLoc i,0 by SCMP_GCD:5 ;
hence s . x = t . x by A1; :: thesis: verum

end;

thus ( x in NAT implies s . x = goto 0 ) :: thesis: ( x = IC SCMPDS implies s . x = inspos 0 )

proof

assume x in NAT ; :: thesis: s . x = goto 0
then reconsider l = x as Instruction-Location of SCMPDS by AMI_1:def 4;
reconsider i = l as Element of NAT by ORDINAL1:def 13;
A3: l = inspos i ;
thus s . x = goto 0 by A1, A3; :: thesis: verum

end;

thus ( x = IC SCMPDS implies s . x = inspos 0 ) by A1; :: thesis: verum

end;

hence for x being set holds
( ( x in SCM-Data-Loc implies s . x = t . x ) & ( x in NAT implies s . x = goto 0 ) & ( x = IC SCMPDS implies s . x = inspos 0 ) ) ; :: thesis: verum