let i1, i2, i3, i4 be Integer; :: thesis: for il being Element of NAT
for s being b₁ -started State-consisting of 0 ,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*> holds
( 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 il -started State-consisting of 0 ,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*> holds
( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 )
let s be il -started State-consisting of 0 ,((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>; :: thesis: ( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 )
set D = ((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>;
A1: ( 0 + 2 = 2 & 0 + 3 = 3 ) ;
A2: ( (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (2 + 1) = i3 & (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (3 + 1) = i4 ) by FINSEQ_1:66;
A3: ( len (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) = 4 & 0 + 0 = 0 ) by FINSEQ_1:66;
( (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (0 + 1) = i1 & (((<*i1*> ^ <*i2*>) ^ <*i3*>) ^ <*i4*>) . (1 + 1) = i2 ) by FINSEQ_1:66;
hence ( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 ) by A2, A3, A1, Def1; :: thesis: verum