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 A1: ( 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 ) ; :: 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*>;

A2: 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) )
assume A3: 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)
( len ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) = 9 & 9 = 8 + 1 ) by FINSEQ_1:92;
then ( k <= 8 & 8 = 7 + 1 ) by A3, NAT_1:13;
then ( ( k <= 7 or k = 8 ) & 7 = 6 + 1 ) by NAT_1:8;
then ( ( k <= 6 or k = 7 or k = 8 ) & 6 = 5 + 1 ) by NAT_1:8;
then ( ( k <= 5 or k = 6 or k = 7 or k = 8 ) & 5 = 4 + 1 ) by NAT_1:8;
then ( ( k <= 4 or k = 5 or k = 6 or k = 7 or k = 8 ) & 4 = 3 + 1 ) by NAT_1:8;
then ( ( k <= 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 ) & 3 = 2 + 1 ) by NAT_1:8;
then ( ( k <= 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 ) & 2 = 1 + 1 ) by NAT_1:8;
then ( ( k <= 1 or k = 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 ) & 1 = 0 + 1 ) by NAT_1:8;
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 ) & 0 <= k ) by NAT_1:8;
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 ) ;
hence s . (il. (0 + k)) = ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) . (k + 1) by A1, 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) )
assume A4: k < len (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) ; :: thesis: s . (dl. (0 + k)) = (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (k + 1)
( len (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) = 4 & 4 = 3 + 1 ) by FINSEQ_1:87;
then ( k <= 3 & 3 = 2 + 1 ) by A4, NAT_1:13;
then ( ( k <= 2 or k = 3 ) & 2 = 1 + 1 ) by NAT_1:8;
then ( ( k <= 1 or k = 2 or k = 3 ) & 1 = 0 + 1 ) by NAT_1:8;
then ( ( k <= 0 or k = 1 or k = 2 or k = 3 ) & 0 <= k ) by NAT_1:8;
then ( k = 0 or k = 1 or k = 2 or k = 3 ) ;
hence s . (dl. (0 + k)) = (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (k + 1) by A1, 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, A2, Def1; :: thesis: verum