let k, n be Nat; :: thesis: for D being set
for f being FinSequence of D
for G being Matrix of D 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 D 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 D st 1 <= k & 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 <= 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:58; :: thesis: verum

end;

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

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 7 :: thesis: ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & [(i29 -' 1),j29] in Indices G & f /. (k + 2) = G * ((i29 -' 1),j29) ) & not ( i19 + 1 = i29 & j19 = j29 & [i29,(j29 + 1)] in Indices G & f /. (k + 2) = G * (i29,(j29 + 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & [i29,(j29 -' 1)] in Indices G & f /. (k + 2) = G * (i29,(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & [(i29 + 1),j29] in Indices G & f /. (k + 2) = G * ((i29 + 1),j29) ) )
A4: len (f | n) = n by A3, FINSEQ_1:59;
then k + 1 in dom (f | n) by A1, SEQ_4:135;
then A5: (f | n) /. (k + 1) = f /. (k + 1) by FINSEQ_4:70;
k + 2 in dom (f | n) by A1, A4, SEQ_4:135;
then A6: (f | n) /. (k + 2) = f /. (k + 2) by FINSEQ_4:70;
k in dom (f | n) by A1, A4, SEQ_4:135;
then (f | n) /. k = f /. k by FINSEQ_4:70;
hence ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & [(i29 -' 1),j29] in Indices G & f /. (k + 2) = G * ((i29 -' 1),j29) ) & not ( i19 + 1 = i29 & j19 = j29 & [i29,(j29 + 1)] in Indices G & f /. (k + 2) = G * (i29,(j29 + 1)) ) & not ( i19 = i29 + 1 & j19 = j29 & [i29,(j29 -' 1)] in Indices G & f /. (k + 2) = G * (i29,(j29 -' 1)) ) implies ( i19 = i29 & j19 = j29 + 1 & [(i29 + 1),j29] in Indices G & f /. (k + 2) = G * ((i29 + 1),j29) ) ) by A2, A5, A6; :: thesis: verum

end;

end;