defpred S1[ set ] means $1 = NAT ;
deffunc H1( set ) -> Element of NAT = il;
consider s being State of SCM ;
defpred S2[ set , set ] means ( ex n being Element of NAT st
( $1 = ps + n & n < len I & $2 = I . n ) or ( $2 = halt SCM & ( for n being Element of NAT holds
( not $1 = ps + n or not n < len I ) ) ) );
deffunc H2( 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
( ( S1[x] implies s1 . x = H1(x) ) & ( not S1[x] implies s1 . x = H2(x) ) ) ) ) from PARTFUN1:sch 1();
 defpred S3[ set ] means ex n being Element of NAT st $1 = n;
A2: for x being set st x in SCM-Memory holds
ex y being set st
( y in SCM-Instr & S2[x,y] )
proof
let x be set ; :: thesis: ( x in SCM-Memory implies ex y being set st
( y in SCM-Instr & S2[x,y] ) )
assume x in SCM-Memory ; :: thesis: ex y being set st
( y in SCM-Instr & S2[x,y] )
per cases ( ex n being Element of NAT st
( x = ps + n & n < len I ) or for n being Element of NAT holds
( not x = ps + n or not n < len I ) ) ;
suppose ex n being Element of NAT st
( x = ps + n & n < len I ) ; :: thesis: ex y being set st
( y in SCM-Instr & S2[x,y] )
then consider n being Element of NAT such that
A3: x = ps + n and
A4: n < len I ;
reconsider y = I . n as Element of the Instructions of SCM by A4, Lm2;
take y ; :: thesis: ( y in SCM-Instr & S2[x,y] )
thus y in SCM-Instr ; :: thesis: S2[x,y]
thus S2[x,y] by A3, A4; :: thesis: verum
end;
suppose A5: for n being Element of NAT holds
( not x = ps + n or not n < len I ) ; :: thesis: ex y being set st
( y in SCM-Instr & S2[x,y] )
take halt SCM ; :: thesis: ( halt SCM in SCM-Instr & S2[x, halt SCM ] )
thus ( halt SCM in SCM-Instr & S2[x, halt SCM ] ) by A5; :: thesis: verum
end;
end;
end;
consider I1 being Function such that
A6: ( dom I1 = SCM-Memory & rng I1 c= SCM-Instr & ( for x being set st x in SCM-Memory holds
S2[x,I1 . x] ) ) from WELLORD2:sch 1(A2);
 reconsider I1 = I1 as Function of SCM-Memory ,the Instructions of SCM by A6, FUNCT_2:def 1, RELSET_1:11;
defpred S4[ 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
( b2 in INT & S4[y,b2] ) )
assume x in SCM-Memory ; :: thesis: ex y being set st
( b2 in INT & S4[y,b2] )
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
( b2 in INT & S4[y,b2] )
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 & S4[x,y] )
thus y in INT by A10, Lm29; :: thesis: S4[x,y]
thus S4[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
( b2 in INT & S4[y,b2] )
hence ex y being set st
( y in INT & S4[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
S4[x,D1 . x] ) ) from WELLORD2:sch 1(A8);
A13: now
let x be set ; :: thesis: ( x in SCM-Memory implies s1 . b1 in the Object-Kind of SCM . b1 )
assume Z: x in SCM-Memory ; :: thesis: s1 . b1 in the Object-Kind of SCM . b1
then reconsider n = x as Element of SCM-Memory ;
per cases ( x = NAT or x <> NAT ) ;
suppose x = NAT ; :: thesis: s1 . b1 in the Object-Kind of SCM . b1
then ( s1 . n = il & 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;
end;
end;
reconsider D1 = D1 as Function of SCM-Memory ,INT by A11, FUNCT_2:def 1, RELSET_1:11;
deffunc H3( set ) -> set = I1 . $1;
reconsider s1 = s1 as State of SCM by A1, A13, FUNCT_1:def 20, PARTFUN1:def 4, RELAT_1:def 18;
deffunc H4( set ) -> set = s1 . $1;
consider s2 being Function such that
A14: ( dom s2 = SCM-Memory & ( for x being set st x in SCM-Memory holds
( ( S3[x] implies s2 . x = H3(x) ) & ( not S3[x] implies s2 . x = H4(x) ) ) ) ) from PARTFUN1:sch 1();
now
let x be set ; :: thesis: ( x in SCM-Memory implies s2 . b1 in the Object-Kind of SCM . b1 )
assume x in SCM-Memory ; :: thesis: s2 . b1 in the Object-Kind of SCM . b1
then reconsider n = x as Element of SCM-Memory ;
per cases ( ex n being Element of NAT st x = n or for n being Element of NAT holds not x = n ) ;
suppose A15: ex n being Element of NAT st x = n ; :: thesis: s2 . b1 in the Object-Kind of SCM . b1
then reconsider a = x as Element of NAT ;
A16: the Object-Kind of SCM . a = SCM-Instr by AMI_2:11;
s2 . x = I1 . n by A14, A15;
hence s2 . x in the Object-Kind of SCM . x by A16; :: thesis: verum
end;
suppose for n being Element of NAT holds not x = n ; :: thesis: s2 . b1 in the Object-Kind of SCM . b1
then s2 . n = s1 . x by A14;
hence s2 . x in the Object-Kind of SCM . x by A1, FUNCT_1:def 20; :: thesis: verum
end;
end;
end;
then reconsider s2 = s2 as State of SCM by A14, FUNCT_1:def 20, PARTFUN1:def 4, RELAT_1:def 18;
deffunc H5( set ) -> set = s2 . $1;
defpred S5[ set ] means ex n being Element of NAT st $1 = dl. n;
deffunc H6( 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
( ( S5[x] implies s3 . x = H6(x) ) & ( not S5[x] implies s3 . x = H5(x) ) ) ) ) from PARTFUN1:sch 1();
now
let x be set ; :: thesis: ( x in SCM-Memory implies s3 . b1 in the Object-Kind of SCM . b1 )
assume x in SCM-Memory ; :: thesis: s3 . b1 in the Object-Kind of SCM . b1
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 for n being Element of NAT holds not x = dl. n ; :: thesis: s3 . b1 in the Object-Kind of SCM . b1
then X: s3 . n = s2 . x by A17;
dom s2 = 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: ( IC s3 = il & ( for k being Element of NAT st k < len I holds
s3 . (ps + k) = I . k ) & ( for k being Element of NAT st k < len D holds
s3 . (dl. (ds + k)) = D . (k + 1) ) )
thus IC s3 = s2 . NAT by A17, AMI_3:4, Th7
.= s1 . NAT by A14, AMI_3:4, Th7
.= il by A1, AMI_2:30 ; :: thesis: ( ( for k being Element of NAT st k < len I holds
s3 . (ps + k) = I . k ) & ( 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 . (ps + k) = I . k )
Y: ps + k in NAT ;
assume k < len I ; :: thesis: s3 . (ps + k) = I . k
then A20: ex k9 being Element of NAT st
( ps + k = ps + k9 & k9 < len I & I1 . (ps + k) = I . k9 ) by A6, Y;
for n being Element of NAT holds ps + k <> dl. n by AMI_3:56;
hence s3 . (ps + k) = s2 . (ps + k) by A17, Y
.= I . k by A14, A20, Y ;
:: 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 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