let f1, f2 be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( f1 is_sequence_on Gauge (C,n) & f1 /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) & f1 /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) & ( for k being Element of NAT st 1 <= k & k + 2 <= len f1 holds
( ( front_right_cell (f1,k,(Gauge (C,n))) misses C & front_left_cell (f1,k,(Gauge (C,n))) misses C implies f1 turns_left k, Gauge (C,n) ) & ( front_right_cell (f1,k,(Gauge (C,n))) misses C & front_left_cell (f1,k,(Gauge (C,n))) meets C implies f1 goes_straight k, Gauge (C,n) ) & ( front_right_cell (f1,k,(Gauge (C,n))) meets C implies f1 turns_right k, Gauge (C,n) ) ) ) & f2 is_sequence_on Gauge (C,n) & f2 /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) & f2 /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) & ( for k being Element of NAT st 1 <= k & k + 2 <= len f2 holds
( ( front_right_cell (f2,k,(Gauge (C,n))) misses C & front_left_cell (f2,k,(Gauge (C,n))) misses C implies f2 turns_left k, Gauge (C,n) ) & ( front_right_cell (f2,k,(Gauge (C,n))) misses C & front_left_cell (f2,k,(Gauge (C,n))) meets C implies f2 goes_straight k, Gauge (C,n) ) & ( front_right_cell (f2,k,(Gauge (C,n))) meets C implies f2 turns_right k, Gauge (C,n) ) ) ) implies f1 = f2 )
assume that
A1138: f1 is_sequence_on Gauge (C,n) and
A1139: f1 /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) and
A1140: f1 /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) and
A1141: for k being Element of NAT st 1 <= k & k + 2 <= len f1 holds
( ( front_right_cell (f1,k,(Gauge (C,n))) misses C & front_left_cell (f1,k,(Gauge (C,n))) misses C implies f1 turns_left k, Gauge (C,n) ) & ( front_right_cell (f1,k,(Gauge (C,n))) misses C & front_left_cell (f1,k,(Gauge (C,n))) meets C implies f1 goes_straight k, Gauge (C,n) ) & ( front_right_cell (f1,k,(Gauge (C,n))) meets C implies f1 turns_right k, Gauge (C,n) ) ) and
A1142: f2 is_sequence_on Gauge (C,n) and
A1143: f2 /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) and
A1144: f2 /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) and
A1145: for k being Element of NAT st 1 <= k & k + 2 <= len f2 holds
( ( front_right_cell (f2,k,(Gauge (C,n))) misses C & front_left_cell (f2,k,(Gauge (C,n))) misses C implies f2 turns_left k, Gauge (C,n) ) & ( front_right_cell (f2,k,(Gauge (C,n))) misses C & front_left_cell (f2,k,(Gauge (C,n))) meets C implies f2 goes_straight k, Gauge (C,n) ) & ( front_right_cell (f2,k,(Gauge (C,n))) meets C implies f2 turns_right k, Gauge (C,n) ) ) ; :: thesis: f1 = f2
defpred S₁[ Element of NAT ] means f1 | $1 = f2 | $1;
A1146: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

A1147: len f2 > 4 by GOBOARD7:34;
A1148: len f1 > 4 by GOBOARD7:34;
A1149: f1 | 1 = <*(f1 /. 1)*> by FINSEQ_5:20;
let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A1150: f1 | k = f2 | k ; :: thesis: S₁[k + 1]

per cases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25;

suppose k = 0 ; :: thesis: S₁[k + 1]

hence S₁[k + 1] by A1139, A1143, A1149, FINSEQ_5:20; :: thesis: verum

end;

suppose A1151: k = 1 ; :: thesis: S₁[k + 1]

f1 | 2 = <*(f1 /. 1),(f1 /. 2)*> by A1148, FINSEQ_5:81, XXREAL_0:2;
hence S₁[k + 1] by A1139, A1140, A1143, A1144, A1147, A1151, FINSEQ_5:81, XXREAL_0:2; :: thesis: verum

end;

suppose A1152: k > 1 ; :: thesis: S₁[k + 1]

A1153: f2 /. 1 = f2 /. (len f2) by FINSEQ_6:def 1;
A1154: f1 /. 1 = f1 /. (len f1) by FINSEQ_6:def 1;

now :: thesis: S₁[k + 1]

per cases ( len f1 > k or k >= len f1 ) ;

suppose A1155: len f1 > k ; :: thesis: S₁[k + 1]

set m = k -' 1;
A1156: 1 <= k -' 1 by A1152, NAT_D:49;
then A1157: (k -' 1) + 1 = k by NAT_D:43;
then A1158: front_right_cell (f1,(k -' 1),(Gauge (C,n))) = front_right_cell ((f1 | k),(k -' 1),(Gauge (C,n))) by A1138, A1155, A1156, GOBRD13:42;
A1159: k + 1 <= len f1 by A1155, NAT_1:13;

A1160: now :: thesis: not len f2 <= k

A1161: 1 < len f2 by GOBOARD7:34, XXREAL_0:2;
assume A1162: len f2 <= k ; :: thesis: contradiction
then A1163: f2 = f2 | k by FINSEQ_1:58;
then A1164: 1 in dom (f2 | k) by FINSEQ_5:6;
len f2 in dom (f2 | k) by A1163, FINSEQ_5:6;
then A1165: (f1 | k) /. (len f2) = f1 /. (len f2) by A1150, FINSEQ_4:70;
len f2 <= len f1 by A1150, A1163, FINSEQ_5:16;
hence contradiction by A1150, A1154, A1153, A1155, A1162, A1163, A1164, A1165, A1161, FINSEQ_4:70, GOBOARD7:38; :: thesis: verum

end;

then A1166: k + 1 <= len f2 by NAT_1:13;
A1167: front_left_cell (f2,(k -' 1),(Gauge (C,n))) = front_left_cell ((f2 | k),(k -' 1),(Gauge (C,n))) by A1142, A1156, A1157, A1160, GOBRD13:42;
A1168: front_right_cell (f2,(k -' 1),(Gauge (C,n))) = front_right_cell ((f2 | k),(k -' 1),(Gauge (C,n))) by A1142, A1156, A1157, A1160, GOBRD13:42;
A1169: (k -' 1) + (1 + 1) = k + 1 by A1157;
A1170: front_left_cell (f1,(k -' 1),(Gauge (C,n))) = front_left_cell ((f1 | k),(k -' 1),(Gauge (C,n))) by A1138, A1155, A1156, A1157, GOBRD13:42;

now :: thesis: S₁[k + 1]

per cases ( ( front_right_cell (f1,(k -' 1),(Gauge (C,n))) misses C & front_left_cell (f1,(k -' 1),(Gauge (C,n))) misses C ) or ( front_right_cell (f1,(k -' 1),(Gauge (C,n))) misses C & front_left_cell (f1,(k -' 1),(Gauge (C,n))) meets C ) or front_right_cell (f1,(k -' 1),(Gauge (C,n))) meets C ) ;

suppose A1171: ( front_right_cell (f1,(k -' 1),(Gauge (C,n))) misses C & front_left_cell (f1,(k -' 1),(Gauge (C,n))) misses C ) ; :: thesis: S₁[k + 1]

then A1172: f1 turns_left k -' 1, Gauge (C,n) by A1141, A1156, A1159, A1169;
f2 turns_left k -' 1, Gauge (C,n) by A1145, A1150, A1156, A1166, A1158, A1170, A1168, A1167, A1169, A1171;
hence S₁[k + 1] by A1142, A1150, A1152, A1166, A1159, A1172, GOBRD13:47; :: thesis: verum

end;

suppose A1173: ( front_right_cell (f1,(k -' 1),(Gauge (C,n))) misses C & front_left_cell (f1,(k -' 1),(Gauge (C,n))) meets C ) ; :: thesis: S₁[k + 1]

then A1174: f1 goes_straight k -' 1, Gauge (C,n) by A1141, A1156, A1159, A1169;
f2 goes_straight k -' 1, Gauge (C,n) by A1145, A1150, A1156, A1166, A1158, A1170, A1168, A1167, A1169, A1173;
hence S₁[k + 1] by A1142, A1150, A1152, A1166, A1159, A1174, GOBRD13:48; :: thesis: verum

end;

suppose A1175: front_right_cell (f1,(k -' 1),(Gauge (C,n))) meets C ; :: thesis: S₁[k + 1]

then A1176: f1 turns_right k -' 1, Gauge (C,n) by A1141, A1156, A1159, A1169;
f2 turns_right k -' 1, Gauge (C,n) by A1145, A1150, A1156, A1166, A1158, A1168, A1169, A1175;
hence S₁[k + 1] by A1142, A1150, A1152, A1166, A1159, A1176, GOBRD13:46; :: thesis: verum

end;

end;

end;

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

end;

suppose A1177: k >= len f1 ; :: thesis: S₁[k + 1]

A1178: 1 < len f1 by GOBOARD7:34, XXREAL_0:2;
A1179: f1 = f1 | k by A1177, FINSEQ_1:58;
then A1180: 1 in dom (f1 | k) by FINSEQ_5:6;
len f1 in dom (f1 | k) by A1179, FINSEQ_5:6;
then A1181: (f2 | k) /. (len f1) = f2 /. (len f1) by A1150, FINSEQ_4:70;
len f1 <= len f2 by A1150, A1179, FINSEQ_5:16;
then len f2 = len f1 by A1150, A1154, A1153, A1179, A1180, A1181, A1178, FINSEQ_4:70, GOBOARD7:38;
hence S₁[k + 1] by A1150, A1177, A1179, FINSEQ_1:58; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

A1182: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1182, A1146);
hence f1 = f2 by JORDAN9:2; :: thesis: verum