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