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
A1139: f1 is_sequence_on Gauge C,n and
A1140: f1 /. 1 = (Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n) and
A1141: f1 /. 2 = (Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) and
A1142: 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
A1143: f2 is_sequence_on Gauge C,n and
A1144: f2 /. 1 = (Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n) and
A1145: f2 /. 2 = (Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) and
A1146: 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;
A1147: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

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

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

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

hence S₁[k + 1] by A1140, A1144, A1150, FINSEQ_5:23; :: thesis: verum

end;

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

f1 | 2 = <*(f1 /. 1),(f1 /. 2)*> by A1149, FINSEQ_5:84, XXREAL_0:2;
hence S₁[k + 1] by A1140, A1141, A1144, A1145, A1148, A1152, FINSEQ_5:84, XXREAL_0:2; :: thesis: verum

end;

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

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

now

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

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

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

A1161: now

A1162: 1 < len f2 by GOBOARD7:36, XXREAL_0:2;
assume A1163: len f2 <= k ; :: thesis: contradiction
then A1164: f2 = f2 | k by FINSEQ_1:79;
then A1165: 1 in dom (f2 | k) by FINSEQ_5:6;
len f2 in dom (f2 | k) by A1164, FINSEQ_5:6;
then A1166: (f1 | k) /. (len f2) = f1 /. (len f2) by A1151, FINSEQ_4:85;
len f2 <= len f1 by A1151, A1164, FINSEQ_5:18;
hence contradiction by A1151, A1155, A1154, A1156, A1163, A1164, A1165, A1166, A1162, FINSEQ_4:85, GOBOARD7:40; :: thesis: verum

end;

then A1167: k + 1 <= len f2 by NAT_1:13;
A1168: front_left_cell f2,(k -' 1),(Gauge C,n) = front_left_cell (f2 | k),(k -' 1),(Gauge C,n) by A1143, A1157, A1158, A1161, GOBRD13:43;
A1169: front_right_cell f2,(k -' 1),(Gauge C,n) = front_right_cell (f2 | k),(k -' 1),(Gauge C,n) by A1143, A1157, A1158, A1161, GOBRD13:43;
A1170: (k -' 1) + (1 + 1) = k + 1 by A1158;
A1171: front_left_cell f1,(k -' 1),(Gauge C,n) = front_left_cell (f1 | k),(k -' 1),(Gauge C,n) by A1139, A1156, A1157, A1158, GOBRD13:43;

now

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 A1172: ( 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 A1173: f1 turns_left k -' 1, Gauge C,n by A1142, A1157, A1160, A1170;
f2 turns_left k -' 1, Gauge C,n by A1146, A1151, A1157, A1167, A1159, A1171, A1169, A1168, A1170, A1172;
hence S₁[k + 1] by A1143, A1151, A1153, A1167, A1160, A1173, GOBRD13:48; :: thesis: verum

end;

suppose A1174: ( 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 A1175: f1 goes_straight k -' 1, Gauge C,n by A1142, A1157, A1160, A1170;
f2 goes_straight k -' 1, Gauge C,n by A1146, A1151, A1157, A1167, A1159, A1171, A1169, A1168, A1170, A1174;
hence S₁[k + 1] by A1143, A1151, A1153, A1167, A1160, A1175, GOBRD13:49; :: thesis: verum

end;

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

then A1177: f1 turns_right k -' 1, Gauge C,n by A1142, A1157, A1160, A1170;
f2 turns_right k -' 1, Gauge C,n by A1146, A1151, A1157, A1167, A1159, A1169, A1170, A1176;
hence S₁[k + 1] by A1143, A1151, A1153, A1167, A1160, A1177, GOBRD13:47; :: thesis: verum

end;

end;

end;

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

end;

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

A1179: 1 < len f1 by GOBOARD7:36, XXREAL_0:2;
A1180: f1 = f1 | k by A1178, FINSEQ_1:79;
then A1181: 1 in dom (f1 | k) by FINSEQ_5:6;
len f1 in dom (f1 | k) by A1180, FINSEQ_5:6;
then A1182: (f2 | k) /. (len f1) = f2 /. (len f1) by A1151, FINSEQ_4:85;
len f1 <= len f2 by A1151, A1180, FINSEQ_5:18;
then len f2 = len f1 by A1151, A1155, A1154, A1180, A1181, A1182, A1179, FINSEQ_4:85, GOBOARD7:40;
hence S₁[k + 1] by A1151, A1178, A1180, FINSEQ_1:79; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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