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_right k,G holds

f turns_right 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_right k,G holds

f turns_right k,G

let f be FinSequence of D; :: thesis: for G being Matrix of D st 1 <= k & k + 2 <= n & f | n turns_right k,G holds

f turns_right k,G

let G be Matrix of D; :: thesis: ( 1 <= k & k + 2 <= n & f | n turns_right k,G implies f turns_right k,G )

assume that

A1: ( 1 <= k & k + 2 <= n ) and

A2: f | n turns_right k,G ; :: thesis: f turns_right k,G

for f being FinSequence of D

for G being Matrix of D st 1 <= k & k + 2 <= n & f | n turns_right k,G holds

f turns_right 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_right k,G holds

f turns_right k,G

let f be FinSequence of D; :: thesis: for G being Matrix of D st 1 <= k & k + 2 <= n & f | n turns_right k,G holds

f turns_right k,G

let G be Matrix of D; :: thesis: ( 1 <= k & k + 2 <= n & f | n turns_right k,G implies f turns_right k,G )

assume that

A1: ( 1 <= k & k + 2 <= n ) and

A2: f | n turns_right k,G ; :: thesis: f turns_right k,G

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

end;

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

let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 6 :: 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;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