let C be Simple_closed_curve; :: thesis: for n, k being Element of 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 Element of NAT ; :: thesis: ( 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;
assume A1:
n is_sufficiently_large_for C
; :: thesis: ( 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 A2:
( Span C,n is_sequence_on Gauge C,n & (Span C,n) /. 1 = (Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n) & (Span C,n) /. 2 = (Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) )
by JORDAN13:def 1;
defpred S1[ Element of NAT ] means for m being Element of 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 );
A3:
S1[ 0 ]
proof
let m be
Element of
NAT ;
:: thesis: ( 1 <= m & m + 1 <= len ((Span C,n) | 0 ) implies ( right_cell ((Span C,n) | 0 ),m,(Gauge C,n) misses C & left_cell ((Span C,n) | 0 ),m,(Gauge C,n) meets C ) )
assume A4:
( 1
<= m &
m + 1
<= len ((Span C,n) | 0 ) )
;
:: thesis: ( right_cell ((Span C,n) | 0 ),m,(Gauge C,n) misses C & left_cell ((Span C,n) | 0 ),m,(Gauge C,n) meets C )
1
<= m + 1
by NAT_1:12;
then
1
<= len ((Span C,n) | 0 )
by A4, XXREAL_0:2;
then
1
<= 0
by CARD_1:47;
hence
(
right_cell ((Span C,n) | 0 ),
m,
(Gauge C,n) misses C &
left_cell ((Span C,n) | 0 ),
m,
(Gauge C,n) meets C )
;
:: thesis: verum
end;
A5:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
A6:
(Span C,n) | (k + 1) is_sequence_on Gauge C,
n
by A2, GOBOARD1:38;
A7:
(Span C,n) | k is_sequence_on Gauge C,
n
by A2, GOBOARD1:38;
assume A8:
for
m being
Element of
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 )
;
:: thesis: S1[k + 1]
per cases
( k >= len (Span C,n) or k < len (Span C,n) )
;
suppose A9:
k < len (Span C,n)
;
:: thesis: S1[k + 1]then A10:
k + 1
<= len (Span C,n)
by NAT_1:13;
then A11:
len ((Span C,n) | (k + 1)) = k + 1
by FINSEQ_1:80;
A12:
len ((Span C,n) | k) = k
by A9, FINSEQ_1:80;
let m be
Element of
NAT ;
:: thesis: ( 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 A13:
( 1
<= m &
m + 1
<= len ((Span C,n) | (k + 1)) )
;
:: thesis: ( 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 )now per cases
( k = 0 or k = 1 or k > 1 )
by NAT_1:26;
suppose A14:
k = 0
;
:: thesis: ( 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 A11, A13, A14, 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;
:: thesis: verum suppose A15:
k = 1
;
:: thesis: ( 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 i =
X-SpanStart C,
n;
set j =
Y-SpanStart C,
n;
(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 A2, A10, A15, JORDAN8:1;
then A16:
(
((Span C,n) | (k + 1)) /. 1
= (Gauge C,n) * (X-SpanStart C,n),
(Y-SpanStart C,n) &
((Span C,n) | (k + 1)) /. 2
= (Gauge C,n) * ((X-SpanStart C,n) -' 1),
(Y-SpanStart C,n) )
by FINSEQ_4:26;
A17:
(
[(X-SpanStart C,n),(Y-SpanStart C,n)] in Indices (Gauge C,n) &
[((X-SpanStart C,n) -' 1),(Y-SpanStart C,n)] in Indices (Gauge C,n) )
by A1, JORDAN11:8, JORDAN11:9;
1
+ 1
<= m + 1
by A13, XREAL_1:8;
then A18:
m + 1
= 1
+ 1
by A11, A13, A15, XXREAL_0:1;
(X-SpanStart C,n) -' 1
<= X-SpanStart C,
n
by NAT_D:35;
then A19:
(
Y-SpanStart C,
n <> (Y-SpanStart C,n) + 1 &
(X-SpanStart C,n) + 1
<> (X-SpanStart C,n) -' 1 )
by NAT_1:13;
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 A6, A13, A16, A17, A18, GOBRD13:def 2;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A1, JORDAN11:11;
:: thesis: 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 A6, A13, A16, A17, A18, A19, GOBRD13:def 3;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A1, JORDAN11:10;
:: thesis: verum end; suppose A20:
k > 1
;
:: thesis: ( 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 A21:
1
<= (len ((Span C,n) | k)) -' 1
by A12, NAT_D:49;
A22:
((len ((Span C,n) | k)) -' 1) + 1
= len ((Span C,n) | k)
by A12, A20, XREAL_1:237;
then A23:
((len ((Span C,n) | k)) -' 1) + (1 + 1) = (len ((Span C,n) | k)) + 1
;
A24:
len ((Span C,n) | k) <= len (Span C,n)
by FINSEQ_5:18;
now per cases
( m + 1 = len ((Span C,n) | (k + 1)) or m + 1 <> len ((Span C,n) | (k + 1)) )
;
suppose A25:
m + 1
= len ((Span C,n) | (k + 1))
;
:: thesis: ( 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 )consider i1,
j1,
i2,
j2 being
Element of
NAT such that A26:
(
[i1,j1] in Indices (Gauge C,n) &
(Span C,n) /. ((len ((Span C,n) | k)) -' 1) = (Gauge C,n) * i1,
j1 )
and A27:
(
[i2,j2] in Indices (Gauge C,n) &
(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 A2, A9, A12, A21, A22, JORDAN8:6;
A28:
( 1
<= i2 &
i2 <= len (Gauge C,n) & 1
<= j2 &
j2 <= width (Gauge C,n) )
by A27, MATRIX_1:39;
then A29:
(i2 -' 1) + 1
= i2
by XREAL_1:237;
A30:
(j2 -' 1) + 1
= j2
by A28, XREAL_1:237;
(
right_cell ((Span C,n) | k),
((len ((Span C,n) | k)) -' 1),
(Gauge C,n) misses C &
left_cell ((Span C,n) | k),
((len ((Span C,n) | k)) -' 1),
(Gauge C,n) meets C )
by A8, A21, A22;
then A31:
(
right_cell (Span C,n),
((len ((Span C,n) | k)) -' 1),
(Gauge C,n) misses C &
left_cell (Span C,n),
((len ((Span C,n) | k)) -' 1),
(Gauge C,n) meets C )
by A2, A12, A21, A22, A24, GOBRD13:32;
now 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 A32:
(
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 )
;
:: thesis: ( 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 A33:
Span C,
n turns_left (len ((Span C,n) | k)) -' 1,
Gauge C,
n
by A1, A10, A12, A21, A23, JORDAN13:def 1;
now 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 A22, A26, A27, A33, GOBRD13:def 7;
suppose that A34:
(
i1 = i2 &
j1 + 1
= j2 )
and A35:
[(i2 -' 1),j2] in Indices (Gauge C,n)
and A36:
(Span C,n) /. (((len ((Span C,n) | k)) -' 1) + 2) = (Gauge C,n) * (i2 -' 1),
j2
;
:: thesis: ( 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 A2, A21, A22, A24, A26, A27, A32, A34, GOBRD13:35;
then
right_cell (Span C,n),
m,
(Gauge C,n) misses C
by A2, A10, A11, A12, A20, A22, A25, A27, A29, A34, A35, A36, GOBRD13:27;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: left_cell ((Span C,n) | (k + 1)),m,(Gauge C,n) meets C
(
cell (Gauge C,n),
(i1 -' 1),
j1 meets C &
(j1 + 1) -' 1
= j1 )
by A2, A9, A12, A21, A22, A26, A27, A31, A34, GOBRD13:22, NAT_D:34;
then
left_cell (Span C,n),
m,
(Gauge C,n) meets C
by A2, A10, A11, A12, A20, A22, A25, A27, A29, A34, A35, A36, GOBRD13:26;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: verum end; suppose that A37:
(
i1 + 1
= i2 &
j1 = j2 )
and A38:
[i2,(j2 + 1)] in Indices (Gauge C,n)
and A39:
(Span C,n) /. (((len ((Span C,n) | k)) -' 1) + 2) = (Gauge C,n) * i2,
(j2 + 1)
;
:: thesis: ( 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 A2, A21, A22, A24, A26, A27, A32, A37, GOBRD13:37;
then
right_cell (Span C,n),
m,
(Gauge C,n) misses C
by A2, A10, A11, A12, A20, A22, A25, A27, A38, A39, GOBRD13:23;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: left_cell ((Span C,n) | (k + 1)),m,(Gauge C,n) meets C
(
cell (Gauge C,n),
i1,
j2 meets C &
(i1 + 1) -' 1
= i1 )
by A2, A9, A12, A21, A22, A26, A27, A31, A37, GOBRD13:24, NAT_D:34;
then
left_cell (Span C,n),
m,
(Gauge C,n) meets C
by A2, A10, A11, A12, A20, A22, A25, A27, A37, A38, A39, GOBRD13:22;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: verum end; suppose that A40:
(
i1 = i2 + 1 &
j1 = j2 )
and A41:
[i2,(j2 -' 1)] in Indices (Gauge C,n)
and A42:
(Span C,n) /. (((len ((Span C,n) | k)) -' 1) + 2) = (Gauge C,n) * i2,
(j2 -' 1)
;
:: thesis: ( 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 A2, A21, A22, A24, A26, A27, A32, A40, GOBRD13:39;
then
right_cell (Span C,n),
m,
(Gauge C,n) misses C
by A2, A10, A11, A12, A20, A22, A25, A27, A30, A41, A42, GOBRD13:29;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: left_cell ((Span C,n) | (k + 1)),m,(Gauge C,n) meets C
cell (Gauge C,n),
i2,
(j2 -' 1) meets C
by A2, A9, A12, A21, A22, A26, A27, A31, A40, GOBRD13:26;
then
left_cell (Span C,n),
m,
(Gauge C,n) meets C
by A2, A10, A11, A12, A20, A22, A25, A27, A30, A41, A42, GOBRD13:28;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: verum end; suppose that A43:
(
i1 = i2 &
j1 = j2 + 1 )
and A44:
[(i2 + 1),j2] in Indices (Gauge C,n)
and A45:
(Span C,n) /. (((len ((Span C,n) | k)) -' 1) + 2) = (Gauge C,n) * (i2 + 1),
j2
;
:: thesis: ( 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 A2, A21, A22, A24, A26, A27, A32, A43, GOBRD13:41;
then
right_cell (Span C,n),
m,
(Gauge C,n) misses C
by A2, A10, A11, A12, A20, A22, A25, A27, A43, A44, A45, GOBRD13:25;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: left_cell ((Span C,n) | (k + 1)),m,(Gauge C,n) meets C
cell (Gauge C,n),
i1,
j2 meets C
by A2, A9, A12, A21, A22, A26, A27, A31, A43, GOBRD13:28;
then
left_cell (Span C,n),
m,
(Gauge C,n) meets C
by A2, A10, A11, A12, A20, A22, A25, A27, A43, A44, A45, GOBRD13:24;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: verum 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 )
;
:: thesis: verum end; suppose A46:
(
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 )
;
:: thesis: ( 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 A47:
Span C,
n goes_straight (len ((Span C,n) | k)) -' 1,
Gauge C,
n
by A1, A10, A12, A21, A23, JORDAN13:def 1;
now 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 A22, A26, A27, A47, GOBRD13:def 8;
suppose that A48:
(
i1 = i2 &
j1 + 1
= j2 )
and A49:
[i2,(j2 + 1)] in Indices (Gauge C,n)
and A50:
(Span C,n) /. (((len ((Span C,n) | k)) -' 1) + 2) = (Gauge C,n) * i2,
(j2 + 1)
;
:: thesis: ( 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 A2, A21, A22, A24, A26, A27, A46, A48, GOBRD13:36;
then
right_cell (Span C,n),
m,
(Gauge C,n) misses C
by A2, A10, A11, A12, A20, A22, A25, A27, A48, A49, A50, GOBRD13:23;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: left_cell ((Span C,n) | (k + 1)),m,(Gauge C,n) meets C
cell (Gauge C,n),
(i2 -' 1),
j2 meets C
by A2, A9, A12, A21, A22, A26, A27, A46, A48, GOBRD13:35;
then
left_cell (Span C,n),
m,
(Gauge C,n) meets C
by A2, A10, A11, A12, A20, A22, A25, A27, A49, A50, GOBRD13:22;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: verum end; suppose that A51:
(
i1 + 1
= i2 &
j1 = j2 )
and A52:
[(i2 + 1),j2] in Indices (Gauge C,n)
and A53:
(Span C,n) /. (((len ((Span C,n) | k)) -' 1) + 2) = (Gauge C,n) * (i2 + 1),
j2
;
:: thesis: ( 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 A2, A21, A22, A24, A26, A27, A46, A51, GOBRD13:38;
then
right_cell (Span C,n),
m,
(Gauge C,n) misses C
by A2, A10, A11, A12, A20, A22, A25, A27, A51, A52, A53, GOBRD13:25;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: left_cell ((Span C,n) | (k + 1)),m,(Gauge C,n) meets C
cell (Gauge C,n),
(i1 + 1),
j1 meets C
by A2, A9, A12, A21, A22, A26, A27, A46, A51, GOBRD13:37;
then
left_cell (Span C,n),
m,
(Gauge C,n) meets C
by A2, A10, A11, A12, A20, A22, A25, A27, A51, A52, A53, GOBRD13:24;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: verum end; suppose that A54:
(
i1 = i2 + 1 &
j1 = j2 )
and A55:
[(i2 -' 1),j2] in Indices (Gauge C,n)
and A56:
(Span C,n) /. (((len ((Span C,n) | k)) -' 1) + 2) = (Gauge C,n) * (i2 -' 1),
j2
;
:: thesis: ( 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 A2, A21, A22, A24, A26, A27, A46, A54, GOBRD13:40;
then
right_cell (Span C,n),
m,
(Gauge C,n) misses C
by A2, A10, A11, A12, A20, A22, A25, A27, A29, A55, A56, GOBRD13:27;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: left_cell ((Span C,n) | (k + 1)),m,(Gauge C,n) meets C
cell (Gauge C,n),
(i2 -' 1),
(j2 -' 1) meets C
by A2, A9, A12, A21, A22, A26, A27, A46, A54, GOBRD13:39;
then
left_cell (Span C,n),
m,
(Gauge C,n) meets C
by A2, A10, A11, A12, A20, A22, A25, A27, A29, A55, A56, GOBRD13:26;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: verum end; suppose that A57:
(
i1 = i2 &
j1 = j2 + 1 )
and A58:
[i2,(j2 -' 1)] in Indices (Gauge C,n)
and A59:
(Span C,n) /. (((len ((Span C,n) | k)) -' 1) + 2) = (Gauge C,n) * i2,
(j2 -' 1)
;
:: thesis: ( 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 &
(j2 -' 1) + 1
= j2 )
by A2, A21, A22, A24, A26, A27, A28, A46, A57, GOBRD13:42, XREAL_1:237;
then
right_cell (Span C,n),
m,
(Gauge C,n) misses C
by A2, A10, A11, A12, A20, A22, A25, A27, A58, A59, GOBRD13:29;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: left_cell ((Span C,n) | (k + 1)),m,(Gauge C,n) meets C
cell (Gauge C,n),
i2,
(j2 -' 1) meets C
by A2, A9, A12, A21, A22, A26, A27, A46, A57, GOBRD13:41;
then
left_cell (Span C,n),
m,
(Gauge C,n) meets C
by A2, A10, A11, A12, A20, A22, A25, A27, A30, A58, A59, GOBRD13:28;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: verum 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 )
;
:: thesis: verum end; suppose A60:
front_right_cell (Span C,n),
((len ((Span C,n) | k)) -' 1),
(Gauge C,n) meets C
;
:: thesis: ( 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 A61:
Span C,
n turns_right (len ((Span C,n) | k)) -' 1,
Gauge C,
n
by A1, A10, A12, A21, A23, JORDAN13:def 1;
now 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 A22, A26, A27, A61, GOBRD13:def 6;
suppose that A62:
(
i1 = i2 &
j1 + 1
= j2 )
and A63:
[(i2 + 1),j2] in Indices (Gauge C,n)
and A64:
(Span C,n) /. (((len ((Span C,n) | k)) -' 1) + 2) = (Gauge C,n) * (i2 + 1),
j2
;
:: thesis: ( 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 misses C &
(j1 + 1) -' 1
= j1 )
by A2, A21, A22, A24, A26, A27, A31, A62, GOBRD13:23, NAT_D:34;
then
right_cell (Span C,n),
m,
(Gauge C,n) misses C
by A2, A10, A11, A12, A20, A22, A25, A27, A62, A63, A64, GOBRD13:25;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: left_cell ((Span C,n) | (k + 1)),m,(Gauge C,n) meets C
cell (Gauge C,n),
i2,
j2 meets C
by A2, A9, A12, A21, A22, A26, A27, A60, A62, GOBRD13:36;
then
left_cell (Span C,n),
m,
(Gauge C,n) meets C
by A2, A10, A11, A12, A20, A22, A25, A27, A63, A64, GOBRD13:24;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: verum suppose that A65:
(
i1 + 1
= i2 &
j1 = j2 )
and A66:
[i2,(j2 -' 1)] in Indices (Gauge C,n)
and A67:
(Span C,n) /. (((len ((Span C,n) | k)) -' 1) + 2) = (Gauge C,n) * i2,
(j2 -' 1)
;
:: thesis: ( 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 &
(i1 + 1) -' 1
= i1 )
by A2, A21, A22, A24, A26, A27, A31, A65, GOBRD13:25, NAT_D:34;
then
right_cell (Span C,n),
m,
(Gauge C,n) misses C
by A2, A10, A11, A12, A20, A22, A25, A27, A30, A65, A66, A67, GOBRD13:29;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: left_cell ((Span C,n) | (k + 1)),m,(Gauge C,n) meets C
cell (Gauge C,n),
i2,
(j2 -' 1) meets C
by A2, A9, A12, A21, A22, A26, A27, A60, A65, GOBRD13:38;
then
left_cell (Span C,n),
m,
(Gauge C,n) meets C
by A2, A10, A11, A12, A20, A22, A25, A27, A30, A66, A67, GOBRD13:28;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: verum suppose that A68:
(
i1 = i2 + 1 &
j1 = j2 )
and A69:
[i2,(j2 + 1)] in Indices (Gauge C,n)
and A70:
(Span C,n) /. (((len ((Span C,n) | k)) -' 1) + 2) = (Gauge C,n) * i2,
(j2 + 1)
;
:: thesis: ( 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 A2, A21, A22, A24, A26, A27, A31, A68, GOBRD13:27;
then
right_cell (Span C,n),
m,
(Gauge C,n) misses C
by A2, A10, A11, A12, A20, A22, A25, A27, A69, A70, GOBRD13:23;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: left_cell ((Span C,n) | (k + 1)),m,(Gauge C,n) meets C
cell (Gauge C,n),
(i2 -' 1),
j2 meets C
by A2, A9, A12, A21, A22, A26, A27, A60, A68, GOBRD13:40;
then
left_cell (Span C,n),
m,
(Gauge C,n) meets C
by A2, A10, A11, A12, A20, A22, A25, A27, A69, A70, GOBRD13:22;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: verum end; suppose that A71:
(
i1 = i2 &
j1 = j2 + 1 )
and A72:
[(i2 -' 1),j2] in Indices (Gauge C,n)
and A73:
(Span C,n) /. (((len ((Span C,n) | k)) -' 1) + 2) = (Gauge C,n) * (i2 -' 1),
j2
;
:: thesis: ( 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 A2, A21, A22, A24, A26, A27, A31, A71, GOBRD13:29;
then
right_cell (Span C,n),
m,
(Gauge C,n) misses C
by A2, A10, A11, A12, A20, A22, A25, A27, A29, A72, A73, GOBRD13:27;
hence
right_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) misses C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: left_cell ((Span C,n) | (k + 1)),m,(Gauge C,n) meets C
cell (Gauge C,n),
(i2 -' 1),
(j2 -' 1) meets C
by A2, A9, A12, A21, A22, A26, A27, A60, A71, GOBRD13:42;
then
left_cell (Span C,n),
m,
(Gauge C,n) meets C
by A2, A10, A11, A12, A20, A22, A25, A27, A29, A72, A73, GOBRD13:26;
hence
left_cell ((Span C,n) | (k + 1)),
m,
(Gauge C,n) meets C
by A2, A10, A11, A13, A25, GOBRD13:32;
:: thesis: verum 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 )
;
:: thesis: verum 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 )
;
:: thesis: verum end; suppose
m + 1
<> len ((Span C,n) | (k + 1))
;
:: thesis: ( 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 A13, XXREAL_0:1;
then A74:
m + 1
<= len ((Span C,n) | k)
by A11, A12, NAT_1:13;
then consider i1,
j1,
i2,
j2 being
Element of
NAT such that A75:
(
[i1,j1] in Indices (Gauge C,n) &
((Span C,n) | k) /. m = (Gauge C,n) * i1,
j1 )
and A76:
(
[i2,j2] in Indices (Gauge C,n) &
((Span C,n) | k) /. (m + 1) = (Gauge C,n) * i2,
j2 )
and A77:
( (
i1 = i2 &
j1 + 1
= j2 ) or (
i1 + 1
= i2 &
j1 = j2 ) or (
i1 = i2 + 1 &
j1 = j2 ) or (
i1 = i2 &
j1 = j2 + 1 ) )
by A7, A13, JORDAN8:6;
A78:
1
<= m + 1
by NAT_1:12;
m <= len ((Span C,n) | k)
by A74, NAT_1:13;
then A79:
(
m in dom ((Span C,n) | k) &
m + 1
in dom ((Span C,n) | k) )
by A13, A74, A78, FINSEQ_3:27;
A80:
(
right_cell ((Span C,n) | k),
m,
(Gauge C,n) misses C &
left_cell ((Span C,n) | k),
m,
(Gauge C,n) meets C )
by A8, A13, A74;
(Span C,n) | (k + 1) = ((Span C,n) | k) ^ <*((Span C,n) /. (k + 1))*>
by A10, JORDAN8:2;
then A81:
(
((Span C,n) | (k + 1)) /. m = (Gauge C,n) * i1,
j1 &
((Span C,n) | (k + 1)) /. (m + 1) = (Gauge C,n) * i2,
j2 )
by A75, A76, A79, FINSEQ_4:83;
now 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 A77;
suppose A82:
(
i1 = i2 &
j1 + 1
= j2 )
;
:: thesis: ( 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
(
right_cell ((Span C,n) | k),
m,
(Gauge C,n) = cell (Gauge C,n),
i1,
j1 &
left_cell ((Span C,n) | k),
m,
(Gauge C,n) = cell (Gauge C,n),
(i1 -' 1),
j1 )
by A7, A13, A74, A75, A76, GOBRD13:22, GOBRD13:23;
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 A6, A13, A75, A76, A80, A81, A82, GOBRD13:22, GOBRD13:23;
:: thesis: verum end; suppose A83:
(
i1 + 1
= i2 &
j1 = j2 )
;
:: thesis: ( 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
(
right_cell ((Span C,n) | k),
m,
(Gauge C,n) = cell (Gauge C,n),
i1,
(j1 -' 1) &
left_cell ((Span C,n) | k),
m,
(Gauge C,n) = cell (Gauge C,n),
i1,
j1 )
by A7, A13, A74, A75, A76, GOBRD13:24, GOBRD13:25;
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 A6, A13, A75, A76, A80, A81, A83, GOBRD13:24, GOBRD13:25;
:: thesis: verum end; suppose A84:
(
i1 = i2 + 1 &
j1 = j2 )
;
:: thesis: ( 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
(
right_cell ((Span C,n) | k),
m,
(Gauge C,n) = cell (Gauge C,n),
i2,
j2 &
left_cell ((Span C,n) | k),
m,
(Gauge C,n) = cell (Gauge C,n),
i2,
(j2 -' 1) )
by A7, A13, A74, A75, A76, GOBRD13:26, GOBRD13:27;
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 A6, A13, A75, A76, A80, A81, A84, GOBRD13:26, GOBRD13:27;
:: thesis: verum end; suppose A85:
(
i1 = i2 &
j1 = j2 + 1 )
;
:: thesis: ( 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
(
right_cell ((Span C,n) | k),
m,
(Gauge C,n) = cell (Gauge C,n),
(i2 -' 1),
j2 &
left_cell ((Span C,n) | k),
m,
(Gauge C,n) = cell (Gauge C,n),
i1,
j2 )
by A7, A13, A74, A75, A76, GOBRD13:28, GOBRD13:29;
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 A6, A13, A75, A76, A80, A81, A85, GOBRD13:28, GOBRD13:29;
:: thesis: verum 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 )
;
:: thesis: verum 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 )
;
:: thesis: verum 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 )
;
:: thesis: verum end;
end;
A86:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A3, A5);
(Span C,n) | (len (Span C,n)) = Span C,n
by FINSEQ_1:79;
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 A86; :: thesis: verum