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 & s . 0 = I1 & s . 1 = I2 & s . 2 = I3 & s . 3 = I4 & s . 4 = I5 & s . 5 = I6 & s . 6 = I7 & s . 7 = I8 & s . 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 & s . 0 = I1 & s . 1 = I2 & s . 2 = I3 & s . 3 = I4 & s . 4 = I5 & s . 5 = I6 & s . 6 = I7 & s . 7 = I8 & s . 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 & s . 0 = I1 & s . 1 = I2 & s . 2 = I3 & s . 3 = I4 & s . 4 = I5 & s . 5 = I6 & s . 6 = I7 & s . 7 = I8 & s . 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 & s . 0 = I1 & s . 1 = I2 & s . 2 = I3 & s . 3 = I4 & s . 4 = I5 & s . 5 = I6 & s . 6 = I7 & s . 7 = I8 & s . 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 and
A2: ( s . 0 = I1 & s . 1 = I2 & s . 2 = I3 & s . 3 = I4 & s . 4 = I5 & s . 5 = I6 & s . 6 = I7 & s . 7 = I8 & s . 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 . (0 + k) = ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . k )
A5: ( len ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) = 9 & 9 = 8 + 1 ) by AFINSQ_1:54;
A6: 8 = 7 + 1 ;
assume k < len ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) ; :: thesis: s . (0 + k) = ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . k
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 . (0 + k) = ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . k by A2, AFINSQ_1:54; :: 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