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-consisting of il, 0 , 0 ,(((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*> holds
( 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 )
let i1, i2, i3, i4 be Integer; :: thesis: for il being Element of NAT
for s being State-consisting of il, 0 , 0 ,(((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*> holds
( 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 )
let il be Element of NAT ; :: thesis: for s being State-consisting of il, 0 , 0 ,(((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*> holds
( 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 )
let s be State-consisting of il, 0 , 0 ,(((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>; :: 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 )
set I = (((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>;
set D = ((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>;
A1: ( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 2 = I3 & ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 3 = I4 ) by AFINSQ_1:54;
A2: ( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 6 = I7 & ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 7 = I8 ) by AFINSQ_1:54;
thus IC s = il by Def1; :: thesis: ( 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 )
A3: ( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 4 = I5 & ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 5 = I6 ) by AFINSQ_1:54;
A4: ( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 8 = I9 & len ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) = 9 ) by AFINSQ_1:54;
A5: ( 0 + 7 = 7 & 0 + 8 = 8 ) ;
A6: ( 0 + 5 = 5 & 0 + 6 = 6 ) ;
A7: ( 0 + 2 = 2 & 0 + 3 = 3 ) ;
A8: ( 0 + 3 = 3 & 0 + 4 = 4 ) ;
A9: ( 0 + 0 = 0 & 0 + 2 = 2 & 0 + 1 = 1 ) ;
( ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 0 = I1 & ((((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%>) . 1 = I2 ) by AFINSQ_1:54;
hence ( 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 ) by A1, A3, A2, A4, A9, A8, A6, A5, Def1; :: thesis: ( s . (dl. 0 ) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 )
A10: ( (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (2 + 1) = i3 & (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (3 + 1) = i4 ) by FINSEQ_1:87;
A11: ( len (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) = 4 & 0 + 0 = 0 ) by FINSEQ_1:87;
( (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (0 + 1) = i1 & (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (1 + 1) = i2 ) by FINSEQ_1:87;
hence ( s . (dl. 0 ) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 ) by A10, A11, A7, Def1; :: thesis: verum