let f1, f2 be non constant standard clockwise_oriented special_circular_sequence; ( 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) ) )
; f1 = f2
defpred S1[ Nat] means f1 | $1 = f2 | $1;
A1147:
for k being Nat st S1[k] holds
S1[k + 1]
proof
A1148:
len f2 > 4
by GOBOARD7:34;
A1149:
len f1 > 4
by GOBOARD7:34;
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A1151:
f1 | k = f2 | k
;
S1[k + 1]
per cases
( k = 0 or k = 1 or k > 1 )
by NAT_1:25;
suppose A1152:
k = 1
;
S1[k + 1]
f1 | 2
= <*(f1 /. 1),(f1 /. 2)*>
by A1149, FINSEQ_5:81, XXREAL_0:2;
hence
S1[
k + 1]
by A1140, A1141, A1144, A1145, A1148, A1152, FINSEQ_5:81, XXREAL_0:2;
verum end; suppose A1153:
k > 1
;
S1[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 S1[k + 1]per cases
( len f1 > k or k >= len f1 )
;
suppose A1156:
len f1 > k
;
S1[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 not len f2 <= kA1162:
1
< len f2
by GOBOARD7:34, XXREAL_0:2;
assume A1163:
len f2 <= k
;
contradictionthen 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;
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 S1[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 )
;
S1[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
S1[
k + 1]
by A1143, A1151, A1153, A1167, A1160, A1173, GOBRD13:47;
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 )
;
S1[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
S1[
k + 1]
by A1143, A1151, A1153, A1167, A1160, A1175, GOBRD13:48;
verum end; suppose A1176:
front_right_cell (
f1,
(k -' 1),
(Gauge (C,n)))
meets C
;
S1[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
S1[
k + 1]
by A1143, A1151, A1153, A1167, A1160, A1177, GOBRD13:46;
verum end; end; end; hence
S1[
k + 1]
;
verum end; suppose A1178:
k >= len f1
;
S1[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
S1[
k + 1]
by A1151, A1178, A1180, FINSEQ_1:58;
verum end; end; end; hence
S1[
k + 1]
;
verum end; end;
end;
A1183:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A1183, A1147);
hence
f1 = f2
by JORDAN9:2; verum