let k, n be Element of NAT ; :: thesis: for D being set
for f being FinSequence of D
for G being Matrix of D st 1 <= k & k + 2 <= len f & k + 2 <= n & f | n turns_left k,G holds
f turns_left k,G
let D be set ; :: thesis: for f being FinSequence of D
for G being Matrix of D st 1 <= k & k + 2 <= len f & k + 2 <= n & f | n turns_left k,G holds
f turns_left k,G
let f be FinSequence of D; :: thesis: for G being Matrix of D st 1 <= k & k + 2 <= len f & k + 2 <= n & f | n turns_left k,G holds
f turns_left k,G
let G be Matrix of D; :: thesis: ( 1 <= k & k + 2 <= len f & k + 2 <= n & f | n turns_left k,G implies f turns_left k,G )
assume that
A1: ( 1 <= k & k + 2 <= len f ) and
A2: k + 2 <= n and
A3: f | n turns_left k,G ; :: thesis: f turns_left k,G

per cases ( len f <= n or n < len f ) ;

suppose len f <= n ; :: thesis: f turns_left k,G

hence f turns_left k,G by A3, FINSEQ_1:79; :: thesis: verum

end;

suppose n < len f ; :: thesis: f turns_left k,G

then len (f | n) = n by FINSEQ_1:80;
then ( k in dom (f | n) & k + 1 in dom (f | n) & k + 2 in dom (f | n) ) by A1, A2, GOBOARD2:4;
then A4: ( (f | n) /. k = f /. k & (f | n) /. (k + 1) = f /. (k + 1) & (f | n) /. (k + 2) = f /. (k + 2) ) by FINSEQ_4:85;
let i1', j1', i2', j2' be Element of NAT ; :: according to GOBRD13:def 7 :: thesis: ( [i1',j1'] in Indices G & [i2',j2'] in Indices G & f /. k = G * i1',j1' & f /. (k + 1) = G * i2',j2' & not ( i1' = i2' & j1' + 1 = j2' & [(i2' -' 1),j2'] in Indices G & f /. (k + 2) = G * (i2' -' 1),j2' ) & not ( i1' + 1 = i2' & j1' = j2' & [i2',(j2' + 1)] in Indices G & f /. (k + 2) = G * i2',(j2' + 1) ) & not ( i1' = i2' + 1 & j1' = j2' & [i2',(j2' -' 1)] in Indices G & f /. (k + 2) = G * i2',(j2' -' 1) ) implies ( i1' = i2' & j1' = j2' + 1 & [(i2' + 1),j2'] in Indices G & f /. (k + 2) = G * (i2' + 1),j2' ) )
thus ( [i1',j1'] in Indices G & [i2',j2'] in Indices G & f /. k = G * i1',j1' & f /. (k + 1) = G * i2',j2' & not ( i1' = i2' & j1' + 1 = j2' & [(i2' -' 1),j2'] in Indices G & f /. (k + 2) = G * (i2' -' 1),j2' ) & not ( i1' + 1 = i2' & j1' = j2' & [i2',(j2' + 1)] in Indices G & f /. (k + 2) = G * i2',(j2' + 1) ) & not ( i1' = i2' + 1 & j1' = j2' & [i2',(j2' -' 1)] in Indices G & f /. (k + 2) = G * i2',(j2' -' 1) ) implies ( i1' = i2' & j1' = j2' + 1 & [(i2' + 1),j2'] in Indices G & f /. (k + 2) = G * (i2' + 1),j2' ) ) by A3, A4, Def7; :: thesis: verum

end;

end;