defpred S₁[ set , set ] means ( ex n being Element of NAT st
( $1 = il. (ps + n) & n < len I & $2 = I . (n + 1) ) or ( $2 = halt SCM & ( for n being Element of NAT holds
( not $1 = il. (ps + n) or not n < len I ) ) ) );
A1: for x being set st x in SCM-Memory holds
ex y being set st
( y in SCM-Instr & S₁[x,y] )

proof

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

per cases ( ex n being Element of NAT st
( x = il. (ps + n) & n < len I ) or for n being Element of NAT holds
( not x = il. (ps + n) or not n < len I ) ) ;

suppose ex n being Element of NAT st
( x = il. (ps + n) & n < len I ) ; :: thesis: ex y being set st
( y in SCM-Instr & S₁[x,y] )

then consider n being Element of NAT such that
A2: ( x = il. (ps + n) & n < len I ) ;
reconsider y = I . (n + 1) as Element of the Instructions of SCM by A2, Lm2;
take y ; :: thesis: ( y in SCM-Instr & S₁[x,y] )
thus y in SCM-Instr ; :: thesis: S₁[x,y]
thus S₁[x,y] by A2; :: thesis: verum

end;

suppose A3: for n being Element of NAT holds
( not x = il. (ps + n) or not n < len I ) ; :: thesis: ex y being set st
( y in SCM-Instr & S₁[x,y] )

reconsider y = halt SCM as Element of the Instructions of SCM ;
take y ; :: thesis: ( y in SCM-Instr & S₁[x,y] )
thus y in SCM-Instr ; :: thesis: S₁[x,y]
thus S₁[x,y] by A3; :: thesis: verum

end;

end;

end;

consider I1 being Function such that
A4: ( dom I1 = SCM-Memory & rng I1 c= SCM-Instr & ( for x being set st x in SCM-Memory holds
S₁[x,I1 . x] ) ) from WELLORD2:sch 1(A1);
reconsider I1 = I1 as Function of SCM-Memory ,the Instructions of SCM by A4, FUNCT_2:def 1, RELSET_1:11;
A5: 0 in INT by INT_1:def 2;
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 ) ) ) );

A6: 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
A7: ( x = dl. (ds + n) & n < len D ) ;
take y = D . (n + 1); :: thesis: ( y in INT & S₂[x,y] )
thus y in INT by A7, Lm2; :: thesis: S₂[x,y]
thus S₂[x,y] by A7; :: 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 A5; :: thesis: verum

end;

end;

end;

consider D1 being Function such that
A8: ( 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(A6);
reconsider D1 = D1 as Function of SCM-Memory ,INT by A8, FUNCT_2:def 1, RELSET_1:11;
A9: dom the Object-Kind of SCM = SCM-Memory by FUNCT_2:def 1;
consider s being State of SCM ;
deffunc H₁( set ) -> Instruction-Location of SCM = il. il;
deffunc H₂( set ) -> set = s . $1;
defpred S₃[ set ] means $1 = NAT ;
consider s1 being Function such that
A10: ( 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();

now

let x be set ; :: thesis: ( x in SCM-Memory implies s1 . b₁ in the Object-Kind of SCM . b₁ )
assume 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 = il. il & the Object-Kind of SCM . x = NAT ) by A10, 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 s1 . n = s . x by A10;
hence s1 . x in the Object-Kind of SCM . x by A9, CARD_3:18; :: thesis: verum

end;

end;

end;

then reconsider s1 = s1 as State of SCM by A9, A10, CARD_3:18;
deffunc H₃( set ) -> set = I1 . $1;
deffunc H₄( set ) -> set = s1 . $1;
defpred S₄[ set ] means ex n being Element of NAT st $1 = il. n;
consider s2 being Function such that
A11: ( dom s2 = SCM-Memory & ( for x being set st x in SCM-Memory holds
( ( S₄[x] implies s2 . x = H₃(x) ) & ( not S₄[x] implies s2 . x = H₄(x) ) ) ) ) from PARTFUN1:sch 1();

now

let x be set ; :: thesis: ( x in SCM-Memory implies s2 . b₁ in the Object-Kind of SCM . b₁ )
assume x in SCM-Memory ; :: thesis: s2 . 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 = il. n or for n being Element of NAT holds not x = il. n ) ;

suppose A12: ex n being Element of NAT st x = il. n ; :: thesis: s2 . b₁ in the Object-Kind of SCM . b₁

then A13: ( s2 . x = I1 . n & x is Instruction-Location of SCM ) by A11;
reconsider a = x as Element of NAT by A12;
the Object-Kind of SCM . a = SCM-Instr by AMI_2:11;
hence s2 . x in the Object-Kind of SCM . x by A13; :: thesis: verum

end;

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

then s2 . n = s1 . x by A11;
hence s2 . x in the Object-Kind of SCM . x by A9, CARD_3:18; :: thesis: verum

end;

end;

end;

then reconsider s2 = s2 as State of SCM by A9, A11, CARD_3:18;
deffunc H₅( set ) -> set = D1 . $1;
deffunc H₆( set ) -> set = s2 . $1;
defpred S₅[ set ] means ex n being Element of NAT st $1 = dl. n;
consider s3 being Function such that
A14: ( 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 ex n being Element of NAT st x = dl. n ; :: thesis: s3 . b₁ in the Object-Kind of SCM . b₁

then A15: ( s3 . x = D1 . n & x in SCM-Data-Loc ) by A14, AMI_3:def 2;
then the Object-Kind of SCM . x = INT by AMI_2:10;
hence s3 . x in the Object-Kind of SCM . x by A15; :: 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 s3 . n = s2 . x by A14;
hence s3 . x in the Object-Kind of SCM . x by A9, CARD_3:18; :: thesis: verum

end;

end;

end;

then reconsider s3 = s3 as State of SCM by A9, A14, CARD_3:18;
take s3 ; :: thesis: ( IC s3 = il. il & ( for k being Element of NAT st k < len I holds
s3 . (il. (ps + k)) = I . (k + 1) ) & ( for k being Element of NAT st k < len D holds
s3 . (dl. (ds + k)) = D . (k + 1) ) )
thus IC s3 = s2 . NAT by A14, Th7, AMI_3:4
.= s1 . NAT by A11, Th7, AMI_3:4
.= il. il by A10, AMI_2:30 ; :: thesis: ( ( for k being Element of NAT st k < len I holds
s3 . (il. (ps + k)) = I . (k + 1) ) & ( for k being Element of NAT st k < len D holds
s3 . (dl. (ds + k)) = D . (k + 1) ) )

hereby :: 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 I implies s3 . (il. (ps + k)) = I . (k + 1) )
assume Z: k < len I ; :: thesis: s3 . (il. (ps + k)) = I . (k + 1)
consider k' being Element of NAT such that
A16: ( il. (ps + k) = il. (ps + k') & k' < len I & I1 . (il. (ps + k)) = I . (k' + 1) ) by A4, Z;
for n being Element of NAT holds il. (ps + k) <> dl. n by AMI_3:56;
hence s3 . (il. (ps + k)) = s2 . (il. (ps + k)) by A14
.= I . (k + 1) by A11, A16 ;
:: thesis: verum

end;

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 k' being Element of NAT such that
A18: ( dl. (ds + k) = dl. (ds + k') & k' < len D & D1 . (dl. (ds + k)) = D . (k' + 1) ) by A8;
ds + k = ds + k' by A18, AMI_3:52;
hence s3 . (dl. (ds + k)) = D . (k + 1) by A14, A18; :: thesis: verum