let I1, I2, I3, I4, I5, I6, I7, I8, I9 be Instruction of SCM ; :: thesis: for i1, i2, i3, i4 being Integer
for il being Element of NAT
for s being State of SCM st IC s = il. il & s . (il. 0 ) = I1 & s . (il. 1) = I2 & s . (il. 2) = I3 & s . (il. 3) = I4 & s . (il. 4) = I5 & s . (il. 5) = I6 & s . (il. 6) = I7 & s . (il. 7) = I8 & s . (il. 8) = I9 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 holds
s is State-consisting of il, 0 , 0 ,(((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>
let i1, i2, i3, i4 be Integer; :: thesis: for il being Element of NAT
for s being State of SCM st IC s = il. il & s . (il. 0 ) = I1 & s . (il. 1) = I2 & s . (il. 2) = I3 & s . (il. 3) = I4 & s . (il. 4) = I5 & s . (il. 5) = I6 & s . (il. 6) = I7 & s . (il. 7) = I8 & s . (il. 8) = I9 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 holds
s is State-consisting of il, 0 , 0 ,(((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>
let il be Element of NAT ; :: thesis: for s being State of SCM st IC s = il. il & s . (il. 0 ) = I1 & s . (il. 1) = I2 & s . (il. 2) = I3 & s . (il. 3) = I4 & s . (il. 4) = I5 & s . (il. 5) = I6 & s . (il. 6) = I7 & s . (il. 7) = I8 & s . (il. 8) = I9 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 holds
s is State-consisting of il, 0 , 0 ,(((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>
let s be State of SCM ; :: thesis: ( IC s = il. il & s . (il. 0 ) = I1 & s . (il. 1) = I2 & s . (il. 2) = I3 & s . (il. 3) = I4 & s . (il. 4) = I5 & s . (il. 5) = I6 & s . (il. 6) = I7 & s . (il. 7) = I8 & s . (il. 8) = I9 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 implies s is State-consisting of il, 0 , 0 ,(((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*> )
assume that
A1: IC s = il. il and
A2: ( s . (il. 0 ) = I1 & s . (il. 1) = I2 & s . (il. 2) = I3 & s . (il. 3) = I4 & s . (il. 4) = I5 & s . (il. 5) = I6 & s . (il. 6) = I7 & s . (il. 7) = I8 & s . (il. 8) = I9 ) and
A3: ( s . (dl. 0 ) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 ) ; :: thesis: s is State-consisting of il, 0 , 0 ,(((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>
set I = (((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>;
set D = ((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>;

A4: now

let k be Element of NAT ; :: thesis: ( k < len ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) implies s . (il. (0 + k)) = ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) . (k + 1) )
A5: ( len ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) = 9 & 9 = 8 + 1 ) by FINSEQ_1:92;
A6: 8 = 7 + 1 ;
assume k < len ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) ; :: thesis: s . (il. (0 + k)) = ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) . (k + 1)
then k <= 8 by A5, NAT_1:13;
then A7: ( k <= 7 or k = 8 ) by A6, NAT_1:8;
A8: 6 = 5 + 1 ;
7 = 6 + 1 ;
then ( k <= 6 or k = 7 or k = 8 ) by A7, NAT_1:8;
then A9: ( k <= 5 or k = 6 or k = 7 or k = 8 ) by A8, NAT_1:8;
A10: 4 = 3 + 1 ;
5 = 4 + 1 ;
then ( k <= 4 or k = 5 or k = 6 or k = 7 or k = 8 ) by A9, NAT_1:8;
then A11: ( k <= 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 ) by A10, NAT_1:8;
A12: 2 = 1 + 1 ;
3 = 2 + 1 ;
then ( k <= 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 ) by A11, NAT_1:8;
then A13: ( k <= 1 or k = 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 ) by A12, NAT_1:8;
1 = 0 + 1 ;
then ( k = 0 or k = 1 or k = 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 ) by A13, NAT_1:8;
hence s . (il. (0 + k)) = ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) . (k + 1) by A2, FINSEQ_1:92; :: thesis: verum

end;

now

let k be Element of NAT ; :: thesis: ( k < len (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) implies s . (dl. (0 + k)) = (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (k + 1) )
A14: ( len (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) = 4 & 4 = 3 + 1 ) by FINSEQ_1:87;
A15: 3 = 2 + 1 ;
assume k < len (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) ; :: thesis: s . (dl. (0 + k)) = (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (k + 1)
then k <= 3 by A14, NAT_1:13;
then A16: ( k <= 2 or k = 3 ) by A15, NAT_1:8;
A17: 1 = 0 + 1 ;
2 = 1 + 1 ;
then ( k <= 1 or k = 2 or k = 3 ) by A16, NAT_1:8;
then ( k = 0 or k = 1 or k = 2 or k = 3 ) by A17, NAT_1:8;
hence s . (dl. (0 + k)) = (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (k + 1) by A3, FINSEQ_1:87; :: thesis: verum

end;

hence s is State-consisting of il, 0 , 0 ,(((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*> by A1, A4, Def1; :: thesis: verum