let k, n be Element of NAT ; :: thesis: for D being set
for f being FinSequence of D
for G being Matrix of st 1 <= k & 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 st 1 <= k & 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 st 1 <= k & k + 2 <= n & f | n turns_left k,G holds
f turns_left k,G
let G be Matrix of ; :: thesis: ( 1 <= k & k + 2 <= n & f | n turns_left k,G implies f turns_left k,G )
assume that
A1: ( 1 <= k & k + 2 <= n ) and
A2: 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 A2, FINSEQ_1:79; :: thesis: verum

end;

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

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' ) )
A4: len (f | n) = n by A3, FINSEQ_1:80;
then k + 1 in dom (f | n) by A1, GOBOARD2:4;
then A5: (f | n) /. (k + 1) = f /. (k + 1) by FINSEQ_4:85;
k + 2 in dom (f | n) by A1, A4, GOBOARD2:4;
then A6: (f | n) /. (k + 2) = f /. (k + 2) by FINSEQ_4:85;
k in dom (f | n) by A1, A4, GOBOARD2:4;
then (f | n) /. k = f /. k by FINSEQ_4:85;
hence ( [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 A2, A5, A6, Def7; :: thesis: verum

end;

end;