let C be Simple_closed_curve; for n, k being Nat st n is_sufficiently_large_for C & 1 <= k & k + 1 <= len (Span (C,n)) holds
( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C )
let n, k be Nat; ( n is_sufficiently_large_for C & 1 <= k & k + 1 <= len (Span (C,n)) implies ( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C ) )
set G = Gauge (C,n);
set f = Span (C,n);
defpred S1[ Nat] means for m being Nat st 1 <= m & m + 1 <= len ((Span (C,n)) | $1) holds
( right_cell (((Span (C,n)) | $1),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | $1),m,(Gauge (C,n))) meets C );
A1:
(Span (C,n)) | (len (Span (C,n))) = Span (C,n)
by FINSEQ_1:58;
assume A2:
n is_sufficiently_large_for C
; ( not 1 <= k or not k + 1 <= len (Span (C,n)) or ( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C ) )
then A3:
Span (C,n) is_sequence_on Gauge (C,n)
by JORDAN13:def 1;
A4:
(Span (C,n)) /. 2 = (Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n)))
by A2, JORDAN13:def 1;
A5:
(Span (C,n)) /. 1 = (Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)))
by A2, JORDAN13:def 1;
A6:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A7:
for
m being
Nat st 1
<= m &
m + 1
<= len ((Span (C,n)) | k) holds
(
right_cell (
((Span (C,n)) | k),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | k),
m,
(Gauge (C,n)))
meets C )
;
S1[k + 1]
A8:
(Span (C,n)) | (k + 1) is_sequence_on Gauge (
C,
n)
by A3, GOBOARD1:22;
A9:
(Span (C,n)) | k is_sequence_on Gauge (
C,
n)
by A3, GOBOARD1:22;
per cases
( k >= len (Span (C,n)) or k < len (Span (C,n)) )
;
suppose A12:
k < len (Span (C,n))
;
S1[k + 1]let m be
Nat;
( 1 <= m & m + 1 <= len ((Span (C,n)) | (k + 1)) implies ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) )assume that A13:
1
<= m
and A14:
m + 1
<= len ((Span (C,n)) | (k + 1))
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )A15:
k + 1
<= len (Span (C,n))
by A12, NAT_1:13;
then A16:
len ((Span (C,n)) | (k + 1)) = k + 1
by FINSEQ_1:59;
A17:
len ((Span (C,n)) | k) = k
by A12, FINSEQ_1:59;
now ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )per cases
( k = 0 or k = 1 or k > 1 )
by NAT_1:25;
suppose A18:
k = 0
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
1
<= m + 1
by NAT_1:12;
then
m + 1
= 0 + 1
by A14, A18, XXREAL_0:1;
hence
(
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C )
by A13;
verum end; suppose A19:
k = 1
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )set j =
Y-SpanStart (
C,
n);
set i =
X-SpanStart (
C,
n);
A20:
(Span (C,n)) | (k + 1) = <*((Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)))),((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))))*>
by A5, A4, A15, A19, FINSEQ_5:81;
then A21:
((Span (C,n)) | (k + 1)) /. 1
= (Gauge (C,n)) * (
(X-SpanStart (C,n)),
(Y-SpanStart (C,n)))
by FINSEQ_4:17;
1
+ 1
<= m + 1
by A13, XREAL_1:6;
then A22:
m + 1
= 1
+ 1
by A16, A14, A19, XXREAL_0:1;
A23:
[((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))] in Indices (Gauge (C,n))
by A2, JORDAN11:9;
A24:
[(X-SpanStart (C,n)),(Y-SpanStart (C,n))] in Indices (Gauge (C,n))
by A2, JORDAN11:8;
(X-SpanStart (C,n)) -' 1
<= X-SpanStart (
C,
n)
by NAT_D:35;
then A25:
(X-SpanStart (C,n)) + 1
<> (X-SpanStart (C,n)) -' 1
by NAT_1:13;
A26:
Y-SpanStart (
C,
n)
<> (Y-SpanStart (C,n)) + 1
;
A27:
((Span (C,n)) | (k + 1)) /. 2
= (Gauge (C,n)) * (
((X-SpanStart (C,n)) -' 1),
(Y-SpanStart (C,n)))
by A20, FINSEQ_4:17;
then
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
= cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
(Y-SpanStart (C,n)))
by A8, A14, A21, A24, A23, A22, A26, A25, GOBRD13:def 2;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A2, JORDAN11:11;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
= cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
((Y-SpanStart (C,n)) -' 1))
by A8, A14, A21, A27, A24, A23, A22, A26, A25, GOBRD13:def 3;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A2, JORDAN11:10;
verum end; suppose A28:
k > 1
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )A29:
len ((Span (C,n)) | k) <= len (Span (C,n))
by FINSEQ_5:16;
A30:
1
<= (len ((Span (C,n)) | k)) -' 1
by A17, A28, NAT_D:49;
A31:
((len ((Span (C,n)) | k)) -' 1) + 1
= len ((Span (C,n)) | k)
by A17, A28, XREAL_1:235;
then A32:
((len ((Span (C,n)) | k)) -' 1) + (1 + 1) = (len ((Span (C,n)) | k)) + 1
;
now ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )per cases
( m + 1 = len ((Span (C,n)) | (k + 1)) or m + 1 <> len ((Span (C,n)) | (k + 1)) )
;
suppose A33:
m + 1
= len ((Span (C,n)) | (k + 1))
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
left_cell (
((Span (C,n)) | k),
((len ((Span (C,n)) | k)) -' 1),
(Gauge (C,n)))
meets C
by A7, A30, A31;
then A34:
left_cell (
(Span (C,n)),
((len ((Span (C,n)) | k)) -' 1),
(Gauge (C,n)))
meets C
by A3, A17, A30, A31, A29, GOBRD13:31;
consider i1,
j1,
i2,
j2 being
Nat such that A35:
[i1,j1] in Indices (Gauge (C,n))
and A36:
(Span (C,n)) /. ((len ((Span (C,n)) | k)) -' 1) = (Gauge (C,n)) * (
i1,
j1)
and A37:
[i2,j2] in Indices (Gauge (C,n))
and A38:
(Span (C,n)) /. (len ((Span (C,n)) | k)) = (Gauge (C,n)) * (
i2,
j2)
and
( (
i1 = i2 &
j1 + 1
= j2 ) or (
i1 + 1
= i2 &
j1 = j2 ) or (
i1 = i2 + 1 &
j1 = j2 ) or (
i1 = i2 &
j1 = j2 + 1 ) )
by A3, A12, A17, A30, A31, JORDAN8:3;
1
<= i2
by A37, MATRIX_0:32;
then A39:
(i2 -' 1) + 1
= i2
by XREAL_1:235;
A40:
1
<= j2
by A37, MATRIX_0:32;
then A41:
(j2 -' 1) + 1
= j2
by XREAL_1:235;
right_cell (
((Span (C,n)) | k),
((len ((Span (C,n)) | k)) -' 1),
(Gauge (C,n)))
misses C
by A7, A30, A31;
then A42:
right_cell (
(Span (C,n)),
((len ((Span (C,n)) | k)) -' 1),
(Gauge (C,n)))
misses C
by A3, A17, A30, A31, A29, GOBRD13:31;
now ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )per cases
( ( front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_left_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C ) or ( front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_left_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ) or front_right_cell ((Span (C,n)),((len ((Span (C,n)) | k)) -' 1),(Gauge (C,n))) meets C )
;
suppose A43:
(
front_right_cell (
(Span (C,n)),
((len ((Span (C,n)) | k)) -' 1),
(Gauge (C,n)))
misses C &
front_left_cell (
(Span (C,n)),
((len ((Span (C,n)) | k)) -' 1),
(Gauge (C,n)))
misses C )
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )then A44:
Span (
C,
n)
turns_left (len ((Span (C,n)) | k)) -' 1,
Gauge (
C,
n)
by A2, A15, A17, A30, A32, JORDAN13:def 1;
now ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )per cases
( ( i1 = i2 & j1 + 1 = j2 & [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ) or ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ) or ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ) )
by A31, A35, A36, A37, A38, A44, GOBRD13:def 7;
suppose that A45:
(
i1 = i2 &
j1 + 1
= j2 )
and A46:
[(i2 -' 1),j2] in Indices (Gauge (C,n))
and A47:
(Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (
(i2 -' 1),
j2)
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell (
(Gauge (C,n)),
(i1 -' 1),
(j1 + 1))
misses C
by A3, A30, A31, A29, A35, A36, A37, A38, A43, A45, GOBRD13:34;
then
right_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A45, A46, A47, GOBRD13:26;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A13, A33, GOBRD13:31;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets CA48:
(j1 + 1) -' 1
= j1
by NAT_D:34;
cell (
(Gauge (C,n)),
(i1 -' 1),
j1)
meets C
by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A45, GOBRD13:21;
then
left_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A45, A46, A47, A48, GOBRD13:25;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A13, A33, GOBRD13:31;
verum end; suppose that A49:
(
i1 + 1
= i2 &
j1 = j2 )
and A50:
[i2,(j2 + 1)] in Indices (Gauge (C,n))
and A51:
(Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (
i2,
(j2 + 1))
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell (
(Gauge (C,n)),
i2,
j2)
misses C
by A3, A30, A31, A29, A35, A36, A37, A38, A43, A49, GOBRD13:36;
then
right_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A50, A51, GOBRD13:22;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A13, A33, GOBRD13:31;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets CA52:
(i1 + 1) -' 1
= i1
by NAT_D:34;
cell (
(Gauge (C,n)),
i1,
j2)
meets C
by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A49, GOBRD13:23;
then
left_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A49, A50, A51, A52, GOBRD13:21;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A13, A33, GOBRD13:31;
verum end; suppose that A53:
(
i1 = i2 + 1 &
j1 = j2 )
and A54:
[i2,(j2 -' 1)] in Indices (Gauge (C,n))
and A55:
(Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (
i2,
(j2 -' 1))
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell (
(Gauge (C,n)),
(i2 -' 1),
(j2 -' 1))
misses C
by A3, A30, A31, A29, A35, A36, A37, A38, A43, A53, GOBRD13:38;
then
right_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A54, A55, GOBRD13:28;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A13, A33, GOBRD13:31;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell (
(Gauge (C,n)),
i2,
(j2 -' 1))
meets C
by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A53, GOBRD13:25;
then
left_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A54, A55, GOBRD13:27;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A13, A33, GOBRD13:31;
verum end; suppose that A56:
(
i1 = i2 &
j1 = j2 + 1 )
and A57:
[(i2 + 1),j2] in Indices (Gauge (C,n))
and A58:
(Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (
(i2 + 1),
j2)
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell (
(Gauge (C,n)),
i1,
(j2 -' 1))
misses C
by A3, A30, A31, A29, A35, A36, A37, A38, A43, A56, GOBRD13:40;
then
right_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A56, A57, A58, GOBRD13:24;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A13, A33, GOBRD13:31;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell (
(Gauge (C,n)),
i1,
j2)
meets C
by A3, A12, A17, A30, A31, A35, A36, A37, A38, A34, A56, GOBRD13:27;
then
left_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A56, A57, A58, GOBRD13:23;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A13, A33, GOBRD13:31;
verum end; end; end; hence
(
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C )
;
verum end; suppose A59:
(
front_right_cell (
(Span (C,n)),
((len ((Span (C,n)) | k)) -' 1),
(Gauge (C,n)))
misses C &
front_left_cell (
(Span (C,n)),
((len ((Span (C,n)) | k)) -' 1),
(Gauge (C,n)))
meets C )
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )then A60:
Span (
C,
n)
goes_straight (len ((Span (C,n)) | k)) -' 1,
Gauge (
C,
n)
by A2, A15, A17, A30, A32, JORDAN13:def 1;
now ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )per cases
( ( i1 = i2 & j1 + 1 = j2 & [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ) or ( i1 + 1 = i2 & j1 = j2 & [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ) or ( i1 = i2 + 1 & j1 = j2 & [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ) or ( i1 = i2 & j1 = j2 + 1 & [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) )
by A31, A35, A36, A37, A38, A60, GOBRD13:def 8;
suppose that A61:
(
i1 = i2 &
j1 + 1
= j2 )
and A62:
[i2,(j2 + 1)] in Indices (Gauge (C,n))
and A63:
(Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (
i2,
(j2 + 1))
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell (
(Gauge (C,n)),
i1,
(j1 + 1))
misses C
by A3, A30, A31, A29, A35, A36, A37, A38, A59, A61, GOBRD13:35;
then
right_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A61, A62, A63, GOBRD13:22;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A13, A33, GOBRD13:31;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell (
(Gauge (C,n)),
(i2 -' 1),
j2)
meets C
by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A61, GOBRD13:34;
then
left_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A62, A63, GOBRD13:21;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A13, A33, GOBRD13:31;
verum end; suppose that A64:
(
i1 + 1
= i2 &
j1 = j2 )
and A65:
[(i2 + 1),j2] in Indices (Gauge (C,n))
and A66:
(Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (
(i2 + 1),
j2)
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell (
(Gauge (C,n)),
(i1 + 1),
(j1 -' 1))
misses C
by A3, A30, A31, A29, A35, A36, A37, A38, A59, A64, GOBRD13:37;
then
right_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A64, A65, A66, GOBRD13:24;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A13, A33, GOBRD13:31;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell (
(Gauge (C,n)),
(i1 + 1),
j1)
meets C
by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A64, GOBRD13:36;
then
left_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A64, A65, A66, GOBRD13:23;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A13, A33, GOBRD13:31;
verum end; suppose that A67:
(
i1 = i2 + 1 &
j1 = j2 )
and A68:
[(i2 -' 1),j2] in Indices (Gauge (C,n))
and A69:
(Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (
(i2 -' 1),
j2)
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell (
(Gauge (C,n)),
(i2 -' 1),
j2)
misses C
by A3, A30, A31, A29, A35, A36, A37, A38, A59, A67, GOBRD13:39;
then
right_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A68, A69, GOBRD13:26;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A13, A33, GOBRD13:31;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell (
(Gauge (C,n)),
(i2 -' 1),
(j2 -' 1))
meets C
by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A67, GOBRD13:38;
then
left_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A68, A69, GOBRD13:25;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A13, A33, GOBRD13:31;
verum end; suppose that A70:
(
i1 = i2 &
j1 = j2 + 1 )
and A71:
[i2,(j2 -' 1)] in Indices (Gauge (C,n))
and A72:
(Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (
i2,
(j2 -' 1))
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )A73:
(j2 -' 1) + 1
= j2
by A40, XREAL_1:235;
cell (
(Gauge (C,n)),
(i2 -' 1),
(j2 -' 1))
misses C
by A3, A30, A31, A29, A35, A36, A37, A38, A59, A70, GOBRD13:41;
then
right_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A71, A72, A73, GOBRD13:28;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A13, A33, GOBRD13:31;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell (
(Gauge (C,n)),
i2,
(j2 -' 1))
meets C
by A3, A12, A17, A30, A31, A35, A36, A37, A38, A59, A70, GOBRD13:40;
then
left_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A71, A72, GOBRD13:27;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A13, A33, GOBRD13:31;
verum end; end; end; hence
(
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C )
;
verum end; suppose A74:
front_right_cell (
(Span (C,n)),
((len ((Span (C,n)) | k)) -' 1),
(Gauge (C,n)))
meets C
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )then A75:
Span (
C,
n)
turns_right (len ((Span (C,n)) | k)) -' 1,
Gauge (
C,
n)
by A2, A15, A17, A30, A32, JORDAN13:def 1;
now ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )per cases
( ( i1 = i2 & j1 + 1 = j2 & [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 + 1),j2) ) or ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (i2,(j2 + 1)) ) or ( i1 = i2 & j1 = j2 + 1 & [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * ((i2 -' 1),j2) ) )
by A31, A35, A36, A37, A38, A75, GOBRD13:def 6;
suppose that A76:
(
i1 = i2 &
j1 + 1
= j2 )
and A77:
[(i2 + 1),j2] in Indices (Gauge (C,n))
and A78:
(Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (
(i2 + 1),
j2)
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )A79:
(j1 + 1) -' 1
= j1
by NAT_D:34;
cell (
(Gauge (C,n)),
i1,
j1)
misses C
by A3, A30, A31, A29, A35, A36, A37, A38, A42, A76, GOBRD13:22;
then
right_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A76, A77, A78, A79, GOBRD13:24;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A13, A33, GOBRD13:31;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell (
(Gauge (C,n)),
i2,
j2)
meets C
by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A76, GOBRD13:35;
then
left_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A77, A78, GOBRD13:23;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A13, A33, GOBRD13:31;
verum end; suppose that A80:
(
i1 + 1
= i2 &
j1 = j2 )
and A81:
[i2,(j2 -' 1)] in Indices (Gauge (C,n))
and A82:
(Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (
i2,
(j2 -' 1))
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )A83:
(i1 + 1) -' 1
= i1
by NAT_D:34;
cell (
(Gauge (C,n)),
i1,
(j1 -' 1))
misses C
by A3, A30, A31, A29, A35, A36, A37, A38, A42, A80, GOBRD13:24;
then
right_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A80, A81, A82, A83, GOBRD13:28;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A13, A33, GOBRD13:31;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell (
(Gauge (C,n)),
i2,
(j2 -' 1))
meets C
by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A80, GOBRD13:37;
then
left_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A41, A81, A82, GOBRD13:27;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A13, A33, GOBRD13:31;
verum end; suppose that A84:
(
i1 = i2 + 1 &
j1 = j2 )
and A85:
[i2,(j2 + 1)] in Indices (Gauge (C,n))
and A86:
(Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (
i2,
(j2 + 1))
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell (
(Gauge (C,n)),
i2,
j2)
misses C
by A3, A30, A31, A29, A35, A36, A37, A38, A42, A84, GOBRD13:26;
then
right_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A85, A86, GOBRD13:22;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A13, A33, GOBRD13:31;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell (
(Gauge (C,n)),
(i2 -' 1),
j2)
meets C
by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A84, GOBRD13:39;
then
left_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A85, A86, GOBRD13:21;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A13, A33, GOBRD13:31;
verum end; suppose that A87:
(
i1 = i2 &
j1 = j2 + 1 )
and A88:
[(i2 -' 1),j2] in Indices (Gauge (C,n))
and A89:
(Span (C,n)) /. (((len ((Span (C,n)) | k)) -' 1) + 2) = (Gauge (C,n)) * (
(i2 -' 1),
j2)
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell (
(Gauge (C,n)),
(i2 -' 1),
j2)
misses C
by A3, A30, A31, A29, A35, A36, A37, A38, A42, A87, GOBRD13:28;
then
right_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A88, A89, GOBRD13:26;
hence
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C
by A3, A15, A16, A13, A33, GOBRD13:31;
left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell (
(Gauge (C,n)),
(i2 -' 1),
(j2 -' 1))
meets C
by A3, A12, A17, A30, A31, A35, A36, A37, A38, A74, A87, GOBRD13:41;
then
left_cell (
(Span (C,n)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A17, A28, A31, A33, A37, A38, A39, A88, A89, GOBRD13:25;
hence
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C
by A3, A15, A16, A13, A33, GOBRD13:31;
verum end; end; end; hence
(
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C )
;
verum end; end; end; hence
(
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C )
;
verum end; suppose
m + 1
<> len ((Span (C,n)) | (k + 1))
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )then
m + 1
< len ((Span (C,n)) | (k + 1))
by A14, XXREAL_0:1;
then A90:
m + 1
<= len ((Span (C,n)) | k)
by A16, A17, NAT_1:13;
then consider i1,
j1,
i2,
j2 being
Nat such that A91:
[i1,j1] in Indices (Gauge (C,n))
and A92:
((Span (C,n)) | k) /. m = (Gauge (C,n)) * (
i1,
j1)
and A93:
[i2,j2] in Indices (Gauge (C,n))
and A94:
((Span (C,n)) | k) /. (m + 1) = (Gauge (C,n)) * (
i2,
j2)
and A95:
( (
i1 = i2 &
j1 + 1
= j2 ) or (
i1 + 1
= i2 &
j1 = j2 ) or (
i1 = i2 + 1 &
j1 = j2 ) or (
i1 = i2 &
j1 = j2 + 1 ) )
by A9, A13, JORDAN8:3;
A96:
right_cell (
((Span (C,n)) | k),
m,
(Gauge (C,n)))
misses C
by A7, A13, A90;
A97:
(Span (C,n)) | (k + 1) = ((Span (C,n)) | k) ^ <*((Span (C,n)) /. (k + 1))*>
by A15, FINSEQ_5:82;
1
<= m + 1
by NAT_1:12;
then
m + 1
in dom ((Span (C,n)) | k)
by A90, FINSEQ_3:25;
then A98:
((Span (C,n)) | (k + 1)) /. (m + 1) = (Gauge (C,n)) * (
i2,
j2)
by A94, A97, FINSEQ_4:68;
A99:
left_cell (
((Span (C,n)) | k),
m,
(Gauge (C,n)))
meets C
by A7, A13, A90;
m <= len ((Span (C,n)) | k)
by A90, NAT_1:13;
then
m in dom ((Span (C,n)) | k)
by A13, FINSEQ_3:25;
then A100:
((Span (C,n)) | (k + 1)) /. m = (Gauge (C,n)) * (
i1,
j1)
by A92, A97, FINSEQ_4:68;
now ( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )per cases
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A95;
suppose A101:
(
i1 = i2 &
j1 + 1
= j2 )
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )then A102:
left_cell (
((Span (C,n)) | k),
m,
(Gauge (C,n)))
= cell (
(Gauge (C,n)),
(i1 -' 1),
j1)
by A9, A13, A90, A91, A92, A93, A94, GOBRD13:21;
right_cell (
((Span (C,n)) | k),
m,
(Gauge (C,n)))
= cell (
(Gauge (C,n)),
i1,
j1)
by A9, A13, A90, A91, A92, A93, A94, A101, GOBRD13:22;
hence
(
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C )
by A8, A13, A14, A91, A93, A96, A99, A100, A98, A101, A102, GOBRD13:21, GOBRD13:22;
verum end; suppose A103:
(
i1 + 1
= i2 &
j1 = j2 )
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )then A104:
left_cell (
((Span (C,n)) | k),
m,
(Gauge (C,n)))
= cell (
(Gauge (C,n)),
i1,
j1)
by A9, A13, A90, A91, A92, A93, A94, GOBRD13:23;
right_cell (
((Span (C,n)) | k),
m,
(Gauge (C,n)))
= cell (
(Gauge (C,n)),
i1,
(j1 -' 1))
by A9, A13, A90, A91, A92, A93, A94, A103, GOBRD13:24;
hence
(
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C )
by A8, A13, A14, A91, A93, A96, A99, A100, A98, A103, A104, GOBRD13:23, GOBRD13:24;
verum end; suppose A105:
(
i1 = i2 + 1 &
j1 = j2 )
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )then A106:
left_cell (
((Span (C,n)) | k),
m,
(Gauge (C,n)))
= cell (
(Gauge (C,n)),
i2,
(j2 -' 1))
by A9, A13, A90, A91, A92, A93, A94, GOBRD13:25;
right_cell (
((Span (C,n)) | k),
m,
(Gauge (C,n)))
= cell (
(Gauge (C,n)),
i2,
j2)
by A9, A13, A90, A91, A92, A93, A94, A105, GOBRD13:26;
hence
(
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C )
by A8, A13, A14, A91, A93, A96, A99, A100, A98, A105, A106, GOBRD13:25, GOBRD13:26;
verum end; suppose A107:
(
i1 = i2 &
j1 = j2 + 1 )
;
( right_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )then A108:
left_cell (
((Span (C,n)) | k),
m,
(Gauge (C,n)))
= cell (
(Gauge (C,n)),
i1,
j2)
by A9, A13, A90, A91, A92, A93, A94, GOBRD13:27;
right_cell (
((Span (C,n)) | k),
m,
(Gauge (C,n)))
= cell (
(Gauge (C,n)),
(i2 -' 1),
j2)
by A9, A13, A90, A91, A92, A93, A94, A107, GOBRD13:28;
hence
(
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C )
by A8, A13, A14, A91, A93, A96, A99, A100, A98, A107, A108, GOBRD13:27, GOBRD13:28;
verum end; end; end; hence
(
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C )
;
verum end; end; end; hence
(
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C )
;
verum end; end; end; hence
(
right_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
misses C &
left_cell (
((Span (C,n)) | (k + 1)),
m,
(Gauge (C,n)))
meets C )
;
verum end; end;
end;
A109:
S1[ 0 ]
by CARD_1:27;
for k being Nat holds S1[k]
from NAT_1:sch 2(A109, A6);
hence
( not 1 <= k or not k + 1 <= len (Span (C,n)) or ( right_cell ((Span (C,n)),k,(Gauge (C,n))) misses C & left_cell ((Span (C,n)),k,(Gauge (C,n))) meets C ) )
by A1; verum