let I1, I2 be Instruction of SCM ; :: thesis: for i1, i2 being Integer
for il being Element of NAT
for s being State-consisting of il, 0 , 0 ,<%I1%> ^ <%I2%>,<*i1*> ^ <*i2*> holds
( IC s = il & s . 0 = I1 & s . 1 = I2 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 )
let i1, i2 be Integer; :: thesis: for il being Element of NAT
for s being State-consisting of il, 0 , 0 ,<%I1%> ^ <%I2%>,<*i1*> ^ <*i2*> holds
( IC s = il & s . 0 = I1 & s . 1 = I2 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 )
let il be Element of NAT ; :: thesis: for s being State-consisting of il, 0 , 0 ,<%I1%> ^ <%I2%>,<*i1*> ^ <*i2*> holds
( IC s = il & s . 0 = I1 & s . 1 = I2 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 )
let s be State-consisting of il, 0 , 0 ,<%I1%> ^ <%I2%>,<*i1*> ^ <*i2*>; :: thesis: ( IC s = il & s . 0 = I1 & s . 1 = I2 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 )
set ins = <%I1%> ^ <%I2%>;
set data = <*i1*> ^ <*i2*>;
A1: 0 + 0 = 0 ;
A2: <*i1*> ^ <*i2*> = <*i1,i2*> by FINSEQ_1:def 9;
then A3: ( len (<*i1*> ^ <*i2*>) = 2 & (<*i1*> ^ <*i2*>) . (0 + 1) = i1 ) by FINSEQ_1:61;
thus IC s = il by Def1; :: thesis: ( s . 0 = I1 & s . 1 = I2 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 )
A4: <%I1%> ^ <%I2%> = <%I1,I2%> ;
then A5: (<%I1%> ^ <%I2%>) . 1 = I2 by AFINSQ_1:42;
A6: (<*i1*> ^ <*i2*>) . (1 + 1) = i2 by A2, FINSEQ_1:61;
( len (<%I1%> ^ <%I2%>) = 2 & (<%I1%> ^ <%I2%>) . 0 = I1 ) by A4, AFINSQ_1:42;
hence ( s . 0 = I1 & s . 1 = I2 & s . (dl. 0 ) = i1 & s . (dl. 1) = i2 ) by A5, A3, A6, A1, Def1; :: thesis: verum