let C be Simple_closed_curve; :: thesis: 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; :: 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);
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 ; :: 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 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; :: thesis: ( 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 ) ; :: thesis: 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 A10: k >= len (Span (C,n)) ; :: thesis: S1[k + 1]
then A11: (Span (C,n)) | (k + 1) = Span (C,n) by FINSEQ_1:58, NAT_1:12;
(Span (C,n)) | k = Span (C,n) by A10, FINSEQ_1:58;
hence S1[k + 1] by A7, A11; :: thesis: verum
end;
suppose A12: k < len (Span (C,n)) ; :: thesis: S1[k + 1]
let m be 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 that
A13: 1 <= m and
A14: 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 )
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 :: 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 )
per cases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25;
suppose A18: 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 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; :: thesis: verum
end;
suppose A19: 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 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; :: 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 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; :: thesis: verum
end;
suppose A28: 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 )
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 :: 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 )
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)) ; :: 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 )
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 :: 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 )
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 ) ; :: 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 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 :: 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 )
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) ; :: 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 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; :: thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
A48: (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; :: thesis: 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)) ; :: 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 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; :: thesis: left_cell (((Span (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
A52: (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; :: thesis: 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)) ; :: 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 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; :: thesis: 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; :: thesis: 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) ; :: 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 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; :: thesis: 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; :: thesis: 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 ) ; :: thesis: 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 ) ; :: 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 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 :: 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 )
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)) ; :: 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 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; :: thesis: 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; :: thesis: 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) ; :: 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 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; :: thesis: 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; :: thesis: 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) ; :: 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 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; :: 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 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; :: thesis: 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)) ; :: 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 )
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; :: thesis: 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; :: thesis: 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 ) ; :: thesis: verum
end;
suppose A74: 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 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 :: 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 )
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) ; :: 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 )
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; :: thesis: 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; :: thesis: 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)) ; :: 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 )
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; :: thesis: 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; :: thesis: 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)) ; :: 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 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; :: thesis: 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; :: thesis: 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) ; :: 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 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; :: 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 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; :: thesis: 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 ) ; :: thesis: 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 ) ; :: 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 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 :: 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 )
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 ) ; :: 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 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; :: thesis: verum
end;
suppose A103: ( 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 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; :: thesis: verum
end;
suppose A105: ( 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 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; :: thesis: verum
end;
suppose A107: ( 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 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; :: thesis: 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 ) ; :: thesis: 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 ) ; :: thesis: 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 ) ; :: thesis: 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; :: thesis: verum