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. 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 )
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. 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 )
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. 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 )
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. 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 )
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 + 1) = I3 & ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) . (3 + 1) = I4 ) by FINSEQ_1:92;
A2: ( ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) . (6 + 1) = I7 & ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) . (7 + 1) = I8 ) by FINSEQ_1:92;
thus IC s = il. il by Def1; :: thesis: ( 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 )
A3: ( ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) . (4 + 1) = I5 & ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) . (5 + 1) = I6 ) by FINSEQ_1:92;
A4: ( ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) . (8 + 1) = I9 & len ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) = 9 ) by FINSEQ_1:92;
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 ) ;
( ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) . (0 + 1) = I1 & ((((((((<*I1*> ^ <*I2*>) ^ <*I3*>) ^ <*I4*>) ^ <*I5*>) ^ <*I6*>) ^ <*I7*>) ^ <*I8*>) ^ <*I9*>) . (1 + 1) = I2 ) by FINSEQ_1:92;
hence ( 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 ) 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