let f1, f2 be non constant standard clockwise_oriented special_circular_sequence; :: thesis:
assume A1009: f1 is_sequence_on Gauge (C,n) ; :: thesis:
defpred S₁[ Element of NAT ] means f1 | $1 = f2 | $1;
given i1 being Element of NAT such that A1010: ( 1 <= i1 & i1 + 1 <= len (Gauge (C,n)) ) and
A1011: f1 /. 1 = (Gauge (C,n)) * (i1,(width (Gauge (C,n)))) and
A1012: f1 /. 2 = (Gauge (C,n)) * ((i1 + 1),(width (Gauge (C,n)))) and
A1013: ( N-min C in cell ((Gauge (C,n)),i1,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i1,((width (Gauge (C,n))) -' 1)) ) ; :: thesis:
assume that
A1014: for k being Element of NAT st 1 <= k & k + 2 <= len f1 holds
( ( front_left_cell (f1,k,(Gauge (C,n))) misses C & front_right_cell (f1,k,(Gauge (C,n))) misses C implies f1 turns_right k, Gauge (C,n) ) & ( front_left_cell (f1,k,(Gauge (C,n))) misses C & front_right_cell (f1,k,(Gauge (C,n))) meets C implies f1 goes_straight k, Gauge (C,n) ) & ( front_left_cell (f1,k,(Gauge (C,n))) meets C implies f1 turns_left k, Gauge (C,n) ) ) and
A1015: f2 is_sequence_on Gauge (C,n) ; :: thesis:
given i2 being Element of NAT such that A1016: ( 1 <= i2 & i2 + 1 <= len (Gauge (C,n)) ) and
A1017: f2 /. 1 = (Gauge (C,n)) * (i2,(width (Gauge (C,n)))) and
A1018: f2 /. 2 = (Gauge (C,n)) * ((i2 + 1),(width (Gauge (C,n)))) and
A1019: ( N-min C in cell ((Gauge (C,n)),i2,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i2,((width (Gauge (C,n))) -' 1)) ) ; :: thesis:
assume A1020: for k being Element of NAT st 1 <= k & k + 2 <= len f2 holds
( ( front_left_cell (f2,k,(Gauge (C,n))) misses C & front_right_cell (f2,k,(Gauge (C,n))) misses C implies f2 turns_right k, Gauge (C,n) ) & ( front_left_cell (f2,k,(Gauge (C,n))) misses C & front_right_cell (f2,k,(Gauge (C,n))) meets C implies f2 goes_straight k, Gauge (C,n) ) & ( front_left_cell (f2,k,(Gauge (C,n))) meets C implies f2 turns_left k, Gauge (C,n) ) ) ; :: thesis:
A1021: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

A1022: len f1 > 4 by GOBOARD7:34;
A1023: ( f1 | 1 = <*(f1 /. 1)*> & f2 | 1 = <*(f2 /. 1)*> ) by FINSEQ_5:20;
A1024: ( i1 = i2 & len f2 > 4 ) by A1010, A1013, A1016, A1019, Th31, GOBOARD7:34;
let k be Element of NAT ; :: thesis:
assume A1025: f1 | k = f2 | k ; :: thesis:

per cases by NAT_1:25;

suppose k = 0 ; :: thesis:

hence S₁[k + 1] by A1010, A1011, A1013, A1016, A1017, A1019, A1023, Th31; :: thesis:

end;

suppose A1026: k = 1 ; :: thesis:

f1 | 2 = <*(f1 /. 1),(f1 /. 2)*> by A1022, FINSEQ_5:81, XXREAL_0:2;
hence S₁[k + 1] by A1011, A1012, A1017, A1018, A1024, A1026, FINSEQ_5:81, XXREAL_0:2; :: thesis:

end;

suppose A1027: k > 1 ; :: thesis:

A1028: ( f1 /. 1 = f1 /. (len f1) & f2 /. 1 = f2 /. (len f2) ) by FINSEQ_6:def 1;

now

per cases ;

suppose A1029: len f1 > k ; :: thesis:

set m = k -' 1;
A1030: 1 <= k -' 1 by A1027, NAT_D:49;
then A1031: (k -' 1) + 1 = k by NAT_D:43;
then A1032: front_left_cell (f1,(k -' 1),(Gauge (C,n))) = front_left_cell ((f1 | k),(k -' 1),(Gauge (C,n))) by A1009, A1029, A1030, GOBRD13:42;
A1033: (k -' 1) + (1 + 1) = k + 1 by A1031;
A1034: k + 1 <= len f1 by A1029, NAT_1:13;

A1035: now

A1036: 1 < len f2 by GOBOARD7:34, XXREAL_0:2;
assume A1037: len f2 <= k ; :: thesis:
then A1038: f2 = f2 | k by FINSEQ_1:58;
then len f2 in dom (f2 | k) by FINSEQ_5:6;
then A1039: (f1 | k) /. (len f2) = f1 /. (len f2) by A1025, FINSEQ_4:70;
( 1 in dom (f2 | k) & len f2 <= len f1 ) by A1025, A1038, FINSEQ_5:6, FINSEQ_5:16;
hence contradiction by A1025, A1028, A1029, A1037, A1038, A1039, A1036, FINSEQ_4:70, GOBOARD7:38; :: thesis:

end;

then A1040: k + 1 <= len f2 by NAT_1:13;
A1041: front_right_cell (f2,(k -' 1),(Gauge (C,n))) = front_right_cell ((f2 | k),(k -' 1),(Gauge (C,n))) by A1015, A1030, A1031, A1035, GOBRD13:42;
A1042: front_left_cell (f2,(k -' 1),(Gauge (C,n))) = front_left_cell ((f2 | k),(k -' 1),(Gauge (C,n))) by A1015, A1030, A1031, A1035, GOBRD13:42;
A1043: front_right_cell (f1,(k -' 1),(Gauge (C,n))) = front_right_cell ((f1 | k),(k -' 1),(Gauge (C,n))) by A1009, A1029, A1030, A1031, GOBRD13:42;

now

per cases ;

suppose ( front_left_cell (f1,(k -' 1),(Gauge (C,n))) misses C & front_right_cell (f1,(k -' 1),(Gauge (C,n))) misses C ) ; :: thesis:

then ( f1 turns_right k -' 1, Gauge (C,n) & f2 turns_right k -' 1, Gauge (C,n) ) by A1014, A1020, A1025, A1030, A1040, A1034, A1032, A1043, A1042, A1041, A1033;
hence S₁[k + 1] by A1015, A1025, A1027, A1040, A1034, GOBRD13:46; :: thesis:

end;

suppose ( front_left_cell (f1,(k -' 1),(Gauge (C,n))) misses C & front_right_cell (f1,(k -' 1),(Gauge (C,n))) meets C ) ; :: thesis:

then ( f1 goes_straight k -' 1, Gauge (C,n) & f2 goes_straight k -' 1, Gauge (C,n) ) by A1014, A1020, A1025, A1030, A1040, A1034, A1032, A1043, A1042, A1041, A1033;
hence S₁[k + 1] by A1015, A1025, A1027, A1040, A1034, GOBRD13:48; :: thesis:

end;

suppose front_left_cell (f1,(k -' 1),(Gauge (C,n))) meets C ; :: thesis:

then ( f1 turns_left k -' 1, Gauge (C,n) & f2 turns_left k -' 1, Gauge (C,n) ) by A1014, A1020, A1025, A1030, A1040, A1034, A1032, A1042, A1033;
hence S₁[k + 1] by A1015, A1025, A1027, A1040, A1034, GOBRD13:47; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

suppose A1044: k >= len f1 ; :: thesis:

A1045: 1 < len f1 by GOBOARD7:34, XXREAL_0:2;
A1046: f1 = f1 | k by A1044, FINSEQ_1:58;
then len f1 in dom (f1 | k) by FINSEQ_5:6;
then A1047: (f2 | k) /. (len f1) = f2 /. (len f1) by A1025, FINSEQ_4:70;
( 1 in dom (f1 | k) & len f1 <= len f2 ) by A1025, A1046, FINSEQ_5:6, FINSEQ_5:16;
then A1048: len f2 = len f1 by A1025, A1028, A1046, A1047, A1045, FINSEQ_4:70, GOBOARD7:38;
A1049: k + 1 > len f1 by A1044, NAT_1:13;
hence f1 | (k + 1) = f1 by FINSEQ_1:58
.= f2 by A1025, A1044, A1046, A1048, FINSEQ_1:58
.= f2 | (k + 1) by A1048, A1049, FINSEQ_1:58 ;
:: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A1050: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1050, A1021);
hence f1 = f2 by Th4; :: thesis: