defpred S₁[ set ] means $1 = NAT ;
deffunc H₁( set ) -> Element of NAT = 0 ;
consider s being State of SCM;
deffunc H₂( set ) -> set = s . $1;
consider s1 being Function such that
A1: ( dom s1 = SCM-Memory & ( for x being set st x in SCM-Memory holds
( ( S₁[x] implies s1 . x = H₁(x) ) & ( not S₁[x] implies s1 . x = H₂(x) ) ) ) ) from PARTFUN1:sch 1();
defpred S₂[ set ] means ex n being Element of NAT st $1 = n;
defpred S₃[ set , set ] means ( ex n being Element of NAT st
( $1 = dl. (ds + n) & n < len D & $2 = D . (n + 1) ) or ( $2 = 0 & ( for n being Element of NAT holds
( not $1 = dl. (ds + n) or not n < len D ) ) ) );
A7: 0 in INT by INT_1:def 2;

A8: now

let x be set ; :: thesis: ( x in SCM-Memory implies ex y being set st
( b₂ in INT & S₃[y,b₂] ) )
assume x in SCM-Memory ; :: thesis: ex y being set st
( b₂ in INT & S₃[y,b₂] )

per cases ( ex n being Element of NAT st
( x = dl. (ds + n) & n < len D ) or for n being Element of NAT holds
( not x = dl. (ds + n) or not n < len D ) ) ;

suppose ex n being Element of NAT st
( x = dl. (ds + n) & n < len D ) ; :: thesis: ex y being set st
( b₂ in INT & S₃[y,b₂] )

then consider n being Element of NAT such that
A9: x = dl. (ds + n) and
A10: n < len D ;
take y = D . (n + 1); :: thesis: ( y in INT & S₃[x,y] )
thus y in INT by A10, Lm29; :: thesis: S₃[x,y]
thus S₃[x,y] by A9, A10; :: thesis: verum

end;

suppose for n being Element of NAT holds
( not x = dl. (ds + n) or not n < len D ) ; :: thesis: ex y being set st
( b₂ in INT & S₃[y,b₂] )

hence ex y being set st
( y in INT & S₃[x,y] ) by A7; :: thesis: verum

end;

end;

end;

consider D1 being Function such that
A11: ( dom D1 = SCM-Memory & rng D1 c= INT & ( for x being set st x in SCM-Memory holds
S₃[x,D1 . x] ) ) from WELLORD2:sch 1(A8);

A13: now

let x be set ; :: thesis: ( x in SCM-Memory implies s1 . b₁ in the Object-Kind of SCM . b₁ )
assume Z: x in SCM-Memory ; :: thesis: s1 . b₁ in the Object-Kind of SCM . b₁
then reconsider n = x as Element of SCM-Memory ;

per cases ( x = NAT or x <> NAT ) ;

suppose x = NAT ; :: thesis: s1 . b₁ in the Object-Kind of SCM . b₁

then ( s1 . n = 0 & the Object-Kind of SCM . x = NAT ) by A1, AMI_2:30, AMI_2:def 5;
hence s1 . x in the Object-Kind of SCM . x ; :: thesis: verum

end;

suppose x <> NAT ; :: thesis: s1 . b₁ in the Object-Kind of SCM . b₁

then X: s1 . n = s . x by A1;
x in dom s by Z, PARTFUN1:def 4;
hence s1 . x in the Object-Kind of SCM . x by X, FUNCT_1:def 20; :: thesis: verum

end;

end;

end;

reconsider D1 = D1 as Function of SCM-Memory,INT by A11, FUNCT_2:def 1, RELSET_1:11;
reconsider s1 = s1 as State of SCM by A1, A13, FUNCT_1:def 20, PARTFUN1:def 4, RELAT_1:def 18;
deffunc H₃( set ) -> set = s1 . $1;
defpred S₄[ set ] means ex n being Element of NAT st $1 = dl. n;
deffunc H₄( set ) -> set = D1 . $1;
consider s3 being Function such that
A17: ( dom s3 = SCM-Memory & ( for x being set st x in SCM-Memory holds
( ( S₄[x] implies s3 . x = H₄(x) ) & ( not S₄[x] implies s3 . x = H₃(x) ) ) ) ) from PARTFUN1:sch 1();

now

let x be set ; :: thesis: ( x in SCM-Memory implies s3 . b₁ in the Object-Kind of SCM . b₁ )
assume x in SCM-Memory ; :: thesis: s3 . b₁ in the Object-Kind of SCM . b₁
then reconsider n = x as Element of SCM-Memory ;

per cases ( ex n being Element of NAT st x = dl. n or for n being Element of NAT holds not x = dl. n ) ;

suppose A18: ex n being Element of NAT st x = dl. n ; :: thesis: s3 . b₁ in the Object-Kind of SCM . b₁

then x in SCM-Data-Loc by AMI_3:def 2;
then A19: the Object-Kind of SCM . x = INT by AMI_2:10;
s3 . x = D1 . n by A17, A18;
hence s3 . x in the Object-Kind of SCM . x by A19; :: thesis: verum

end;

suppose for n being Element of NAT holds not x = dl. n ; :: thesis: s3 . b₁ in the Object-Kind of SCM . b₁

then X: s3 . n = s1 . x by A17;
dom s1 = the carrier of SCM by PARTFUN1:def 4;
hence s3 . x in the Object-Kind of SCM . x by X, FUNCT_1:def 20; :: thesis: verum

end;

end;

end;

then reconsider s3 = s3 as State of SCM by A17, FUNCT_1:def 20, PARTFUN1:def 4, RELAT_1:def 18;
take s3 ; :: thesis: for k being Element of NAT st k < len D holds
s3 . (dl. (ds + k)) = D . (k + 1)
let k be Element of NAT ; :: thesis: ( k < len D implies s3 . (dl. (ds + k)) = D . (k + 1) )
assume k < len D ; :: thesis: s3 . (dl. (ds + k)) = D . (k + 1)
then consider k9 being Element of NAT such that
A21: dl. (ds + k) = dl. (ds + k9) and
k9 < len D and
A22: D1 . (dl. (ds + k)) = D . (k9 + 1) by A11;
ds + k = ds + k9 by A21, AMI_3:52;
hence s3 . (dl. (ds + k)) = D . (k + 1) by A17, A22; :: thesis: verum