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 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 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 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 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₁[ Nat] means f1 | $1 = f2 | $1;
A1147: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

A1148: len f2 > 4 by GOBOARD7:34;
A1149: len f1 > 4 by GOBOARD7:34;
let k be 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:25;

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

( 1 <= len f1 & 1 <= len f2 ) by A1148, A1149, XXREAL_0:2;
then ( 1 in dom f1 & 1 in dom f2 ) by FINSEQ_3:25;
then W2: ( <*(f1 . 1)*> = <*(f1 /. 1)*> & <*(f2 . 1)*> = <*(f2 /. 1)*> ) by PARTFUN1:def 6;
W1: ( <*(f1 . 1)*> = f1 | 1 & <*(f2 . 1)*> = f2 | 1 ) by FINSEQ_5:20;
<*(f1 . 1)*> = <*(f2 . 1)*> by A1140, A1144, W2;
then f1 | 1 = f2 | 1 by W1;
hence S₁[k + 1] by W; :: thesis: verum

end;

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

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

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:42;
A1160: k + 1 <= len f1 by A1156, NAT_1:13;

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

A1162: 1 < len f2 by GOBOARD7:34, XXREAL_0:2;
assume A1163: len f2 <= k ; :: thesis: contradiction
then A1164: f2 = f2 | k by FINSEQ_1:58;
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:70;
len f2 <= len f1 by A1151, A1164, FINSEQ_5:16;
hence contradiction by A1151, A1155, A1154, A1156, A1163, A1164, A1165, A1166, A1162, FINSEQ_4:70, GOBOARD7:38; :: 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:42;
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:42;
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: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 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:47; :: 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:48; :: 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:46; :: 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:34, XXREAL_0:2;
A1180: f1 = f1 | k by A1178, FINSEQ_1:58;
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:70;
len f1 <= len f2 by A1151, A1180, FINSEQ_5:16;
then len f2 = len f1 by A1151, A1155, A1154, A1180, A1181, A1182, A1179, FINSEQ_4:70, GOBOARD7:38;
hence S₁[k + 1] by A1151, A1178, A1180, FINSEQ_1:58; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

A1183: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A1183, A1147);
hence f1 = f2 by JORDAN9:2; :: thesis: verum