let f1, f2 be non constant standard clockwise_oriented special_circular_sequence; :: thesis:
assume A1007: f1 is_sequence_on Gauge (C,n) ; :: thesis:
defpred S₁[ Nat] means f1 | $1 = f2 | $1;
given i1 being Nat such that A1008: ( 1 <= i1 & i1 + 1 <= len (Gauge (C,n)) ) and
A1009: f1 /. 1 = (Gauge (C,n)) * (i1,(width (Gauge (C,n)))) and
A1010: f1 /. 2 = (Gauge (C,n)) * ((i1 + 1),(width (Gauge (C,n)))) and
A1011: ( 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
A1012: for k being 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
A1013: f2 is_sequence_on Gauge (C,n) ; :: thesis:
given i2 being Nat such that A1014: ( 1 <= i2 & i2 + 1 <= len (Gauge (C,n)) ) and
A1015: f2 /. 1 = (Gauge (C,n)) * (i2,(width (Gauge (C,n)))) and
A1016: f2 /. 2 = (Gauge (C,n)) * ((i2 + 1),(width (Gauge (C,n)))) and
A1017: ( 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 A1018: for k being 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:
A1019: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

A1020: len f1 > 4 by GOBOARD7:34;
A1021: ( f1 | 1 = <*(f1 . 1)*> & f2 | 1 = <*(f2 . 1)*> ) by FINSEQ_5:20;
A1022: ( i1 = i2 & len f2 > 4 ) by A1008, A1011, A1014, A1017, Th29, GOBOARD7:34;
( 1 <= len f1 & 1 <= len f2 ) by A1020, A1022, XXREAL_0:2;
then ( 1 in dom f1 & 1 in dom f2 ) by FINSEQ_3:25;
then S: ( f1 . 1 = f1 /. 1 & f2 . 1 = f2 /. 1 ) by PARTFUN1:def 6;
let k be Nat; :: thesis:
assume A1023: f1 | k = f2 | k ; :: thesis:

per cases by NAT_1:25;

suppose k = 0 ; :: thesis:

hence S₁[k + 1] by S, A1008, A1009, A1011, A1014, A1015, A1017, A1021, Th29; :: thesis:

end;

suppose A1024: k = 1 ; :: thesis:

f1 | 2 = <*(f1 /. 1),(f1 /. 2)*> by A1020, FINSEQ_5:81, XXREAL_0:2;
hence S₁[k + 1] by A1009, A1010, A1015, A1016, A1022, A1024, FINSEQ_5:81, XXREAL_0:2; :: thesis:

end;

suppose A1025: k > 1 ; :: thesis:

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

now :: thesis:

per cases ;

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

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

A1033: now :: thesis:

A1034: 1 < len f2 by GOBOARD7:34, XXREAL_0:2;
assume A1035: len f2 <= k ; :: thesis:
then A1036: f2 = f2 | k by FINSEQ_1:58;
then len f2 in dom (f2 | k) by FINSEQ_5:6;
then A1037: (f1 | k) /. (len f2) = f1 /. (len f2) by A1023, FINSEQ_4:70;
( 1 in dom (f2 | k) & len f2 <= len f1 ) by A1023, A1036, FINSEQ_5:6, FINSEQ_5:16;
hence contradiction by A1023, A1026, A1027, A1035, A1036, A1037, A1034, FINSEQ_4:70, GOBOARD7:38; :: thesis:

end;

then A1038: k + 1 <= len f2 by NAT_1:13;
A1039: front_right_cell (f2,(k -' 1),(Gauge (C,n))) = front_right_cell ((f2 | k),(k -' 1),(Gauge (C,n))) by A1013, A1028, A1029, A1033, GOBRD13:42;
A1040: front_left_cell (f2,(k -' 1),(Gauge (C,n))) = front_left_cell ((f2 | k),(k -' 1),(Gauge (C,n))) by A1013, A1028, A1029, A1033, GOBRD13:42;
A1041: front_right_cell (f1,(k -' 1),(Gauge (C,n))) = front_right_cell ((f1 | k),(k -' 1),(Gauge (C,n))) by A1007, A1027, A1028, A1029, GOBRD13:42;

now :: thesis:

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 A1012, A1018, A1023, A1028, A1038, A1032, A1030, A1041, A1040, A1039, A1031;
hence S₁[k + 1] by A1013, A1023, A1025, A1038, A1032, 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 A1012, A1018, A1023, A1028, A1038, A1032, A1030, A1041, A1040, A1039, A1031;
hence S₁[k + 1] by A1013, A1023, A1025, A1038, A1032, 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 A1012, A1018, A1023, A1028, A1038, A1032, A1030, A1040, A1031;
hence S₁[k + 1] by A1013, A1023, A1025, A1038, A1032, GOBRD13:47; :: thesis:

end;

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

end;

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

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

end;

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

end;

A1048: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A1048, A1019);
hence f1 = f2 by Th2; :: thesis: