let C be Simple_closed_curve; :: thesis: for n, k being Element of NAT st n is_sufficiently_large_for C & Y-SpanStart C,n <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 holds
(cell (Gauge C,n),((X-SpanStart C,n) -' 1),k) \ (L~ (Span C,n)) c= BDD (L~ (Span C,n))
let n, k be Element of NAT ; :: thesis: ( n is_sufficiently_large_for C & Y-SpanStart C,n <= k & k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 implies (cell (Gauge C,n),((X-SpanStart C,n) -' 1),k) \ (L~ (Span C,n)) c= BDD (L~ (Span C,n)) )
set G = Gauge C,n;
set f = Span C,n;
set AI = ApproxIndex C;
set YI = Y-InitStart C;
set XS = X-SpanStart C,n;
set YS = Y-SpanStart C,n;
assume that
A1: n is_sufficiently_large_for C and
A2: Y-SpanStart C,n <= k and
A3: k <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 ; :: thesis: (cell (Gauge C,n),((X-SpanStart C,n) -' 1),k) \ (L~ (Span C,n)) c= BDD (L~ (Span C,n))
A4: Span C,n is_sequence_on Gauge C,n by A1, JORDAN13:def 1;
reconsider ro = k - (Y-SpanStart C,n) as Element of NAT by A2, INT_1:18;
A5: ro <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart C,n) by A3, XREAL_1:11;
A6: k = (Y-SpanStart C,n) + ro ;
defpred S1[ Element of NAT ] means ( $1 <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart C,n) implies (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + $1)) \ (L~ (Span C,n)) c= BDD (L~ (Span C,n)) );
A7: 1 <= (X-SpanStart C,n) -' 1 by JORDAN1H:59;
X-SpanStart C,n > 2 by JORDAN1H:58;
then A8: ((X-SpanStart C,n) -' 1) + 1 = X-SpanStart C,n by XREAL_1:237, XXREAL_0:2;
A9: (X-SpanStart C,n) -' 1 < len (Gauge C,n) by JORDAN1H:59;
A10: for t being Element of NAT st S1[t] holds
S1[t + 1]
proof
let t be Element of NAT ; :: thesis: ( S1[t] implies S1[t + 1] )
assume A11: ( t <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart C,n) implies (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + t)) \ (L~ (Span C,n)) c= BDD (L~ (Span C,n)) ) ; :: thesis: S1[t + 1]
set Ls = LSeg ((Gauge C,n) * ((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))),((Gauge C,n) * (X-SpanStart C,n),((Y-SpanStart C,n) + (t + 1)));
A12: t < t + 1 by NAT_1:13;
set p = (1 / 2) * (((Gauge C,n) * ((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) + ((Gauge C,n) * (X-SpanStart C,n),((Y-SpanStart C,n) + (t + 1))));
A13: (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) \ (L~ (Span C,n)) c= (L~ (Span C,n)) `
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) \ (L~ (Span C,n)) or y in (L~ (Span C,n)) ` )
assume A14: y in (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) \ (L~ (Span C,n)) ; :: thesis: y in (L~ (Span C,n)) `
then not y in L~ (Span C,n) by XBOOLE_0:def 5;
hence y in (L~ (Span C,n)) ` by A14, SUBSET_1:50; :: thesis: verum
end;
A15: (1 / 2) * (((Gauge C,n) * ((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) + ((Gauge C,n) * (X-SpanStart C,n),((Y-SpanStart C,n) + (t + 1)))) in LSeg ((Gauge C,n) * ((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))),((Gauge C,n) * (X-SpanStart C,n),((Y-SpanStart C,n) + (t + 1))) by RLTOPSP1:70;
A16: ((Y-SpanStart C,n) + t) + 1 = (Y-SpanStart C,n) + (t + 1) ;
then A17: 1 <= (Y-SpanStart C,n) + (t + 1) by NAT_1:11;
A18: Y-InitStart C > 1 by JORDAN11:2;
then Y-InitStart C >= (1 + 1) + 0 by NAT_1:13;
then (Y-InitStart C) - 2 >= 0 by XREAL_1:21;
then A19: (Y-InitStart C) -' 2 = (Y-InitStart C) - 2 by XREAL_0:def 2;
assume A20: t + 1 <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart C,n) ; :: thesis: (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) \ (L~ (Span C,n)) c= BDD (L~ (Span C,n))
then A21: (t + 1) + (Y-SpanStart C,n) <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by XREAL_1:21;
assume not (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) \ (L~ (Span C,n)) c= BDD (L~ (Span C,n)) ; :: thesis: contradiction
then consider x being set such that
A22: x in (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) \ (L~ (Span C,n)) and
A23: not x in BDD (L~ (Span C,n)) by TARSKI:def 3;
not x in L~ (Span C,n) by A22, XBOOLE_0:def 5;
then x in (L~ (Span C,n)) ` by A22, SUBSET_1:50;
then x in (BDD (L~ (Span C,n))) \/ (UBD (L~ (Span C,n))) by JORDAN2C:31;
then x in UBD (L~ (Span C,n)) by A23, XBOOLE_0:def 3;
then A24: (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) \ (L~ (Span C,n)) meets UBD (L~ (Span C,n)) by A22, XBOOLE_0:3;
A25: Y-InitStart C < width (Gauge C,(ApproxIndex C)) by JORDAN11:def 2;
ApproxIndex C <= n by A1, JORDAN11:def 1;
then ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 < width (Gauge C,n) by A18, A25, JORDAN1A:53;
then A26: ((Y-SpanStart C,n) + t) + 1 <= width (Gauge C,n) by A19, A21, XXREAL_0:2;
A27: ((Y-SpanStart C,n) + t) + 1 <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A21;
A28: now
A29: Y-SpanStart C,n <= (Y-SpanStart C,n) + (t + 1) by NAT_1:11;
A30: X-SpanStart C,n < len (Gauge C,n) by JORDAN1H:58;
assume (1 / 2) * (((Gauge C,n) * ((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) + ((Gauge C,n) * (X-SpanStart C,n),((Y-SpanStart C,n) + (t + 1)))) in L~ (Span C,n) ; :: thesis: contradiction
then consider i being Element of NAT such that
A31: 1 <= i and
A32: i + 1 <= len (Span C,n) and
A33: (1 / 2) * (((Gauge C,n) * ((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) + ((Gauge C,n) * (X-SpanStart C,n),((Y-SpanStart C,n) + (t + 1)))) in LSeg (Span C,n),i by SPPOL_2:13;
A34: LSeg (Span C,n),i = LSeg ((Span C,n) /. i),((Span C,n) /. (i + 1)) by A31, A32, TOPREAL1:def 5;
consider i1, j1, i2, j2 being Element of NAT such that
A35: [i1,j1] in Indices (Gauge C,n) and
A36: (Span C,n) /. i = (Gauge C,n) * i1,j1 and
A37: [i2,j2] in Indices (Gauge C,n) and
A38: (Span C,n) /. (i + 1) = (Gauge C,n) * i2,j2 and
A39: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A4, A31, A32, JORDAN8:6;
A40: 1 <= i1 by A35, MATRIX_1:39;
A41: i2 <= len (Gauge C,n) by A37, MATRIX_1:39;
A42: 1 <= i2 by A37, MATRIX_1:39;
A43: j1 <= width (Gauge C,n) by A35, MATRIX_1:39;
A44: 1 <= j2 by A37, MATRIX_1:39;
A45: i1 <= len (Gauge C,n) by A35, MATRIX_1:39;
A46: j2 <= width (Gauge C,n) by A37, MATRIX_1:39;
A47: 1 <= j1 by A35, MATRIX_1:39;
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 A39;
suppose ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: contradiction
hence contradiction by A7, A8, A26, A17, A33, A34, A36, A38, A40, A45, A47, A46, A30, GOBOARD7:29; :: thesis: verum
end;
suppose A48: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: contradiction
then A49: (Y-SpanStart C,n) + (t + 1) = j1 by A7, A8, A26, A17, A33, A34, A36, A38, A40, A47, A43, A41, A30, GOBOARD7:28;
A50: cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1)) c= BDD C by A1, A21, A29, JORDAN11:def 3;
A51: left_cell (Span C,n),i,(Gauge C,n) = cell (Gauge C,n),i1,j1 by A4, A31, A32, A35, A36, A37, A38, A48, GOBRD13:24;
(X-SpanStart C,n) -' 1 = i1 by A7, A8, A26, A17, A33, A34, A36, A38, A40, A47, A43, A41, A30, A48, GOBOARD7:28;
then cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1)) meets C by A1, A31, A32, A49, A51, Th8;
hence contradiction by A50, JORDAN1A:15, XBOOLE_1:63; :: thesis: verum
end;
suppose A52: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: contradiction
then A53: left_cell (Span C,n),i,(Gauge C,n) = cell (Gauge C,n),i2,(j2 -' 1) by A4, A31, A32, A35, A36, A37, A38, GOBRD13:26;
A54: (Y-SpanStart C,n) + (t + 1) = j2 by A7, A8, A26, A17, A33, A34, A36, A38, A45, A47, A43, A42, A30, A52, GOBOARD7:28;
(X-SpanStart C,n) -' 1 = i2 by A7, A8, A26, A17, A33, A34, A36, A38, A45, A47, A43, A42, A30, A52, GOBOARD7:28;
then cell (Gauge C,n),((X-SpanStart C,n) -' 1),(((Y-SpanStart C,n) + (t + 1)) -' 1) meets C by A1, A31, A32, A54, A53, Th8;
then A55: cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + t) meets C by A16, NAT_D:34;
A56: Y-SpanStart C,n <= (Y-SpanStart C,n) + t by NAT_1:11;
(Y-SpanStart C,n) + t <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A27, NAT_1:13;
then cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + t) c= BDD C by A1, A56, JORDAN11:def 3;
hence contradiction by A55, JORDAN1A:15, XBOOLE_1:63; :: thesis: verum
end;
suppose ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: contradiction
hence contradiction by A7, A8, A26, A17, A33, A34, A36, A38, A40, A45, A43, A44, A30, GOBOARD7:29; :: thesis: verum
end;
end;
end;
(Y-SpanStart C,n) + t < width (Gauge C,n) by A26, NAT_1:13;
then LSeg ((Gauge C,n) * ((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))),((Gauge C,n) * (X-SpanStart C,n),((Y-SpanStart C,n) + (t + 1))) c= cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + t) by A7, A9, A8, A16, GOBOARD5:22;
then A57: (1 / 2) * (((Gauge C,n) * ((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) + ((Gauge C,n) * (X-SpanStart C,n),((Y-SpanStart C,n) + (t + 1)))) in (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + t)) \ (L~ (Span C,n)) by A28, A15, XBOOLE_0:def 5;
LSeg ((Gauge C,n) * ((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))),((Gauge C,n) * (X-SpanStart C,n),((Y-SpanStart C,n) + (t + 1))) c= cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1)) by A7, A9, A8, A26, A17, GOBOARD5:23;
then A58: (1 / 2) * (((Gauge C,n) * ((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) + ((Gauge C,n) * (X-SpanStart C,n),((Y-SpanStart C,n) + (t + 1)))) in (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) \ (L~ (Span C,n)) by A28, A15, XBOOLE_0:def 5;
LeftComp (Span C,n) is_a_component_of (L~ (Span C,n)) ` by GOBOARD9:def 1;
then UBD (L~ (Span C,n)) is_a_component_of (L~ (Span C,n)) ` by GOBRD14:46;
then (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + (t + 1))) \ (L~ (Span C,n)) c= UBD (L~ (Span C,n)) by A4, A9, A26, A24, A13, Th30, GOBOARD9:6;
then BDD (L~ (Span C,n)) meets UBD (L~ (Span C,n)) by A11, A20, A12, A57, A58, XBOOLE_0:3, XXREAL_0:2;
hence contradiction by JORDAN2C:28; :: thesis: verum
end;
A59: S1[ 0 ]
proof
assume 0 <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart C,n) ; :: thesis: (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + 0 )) \ (L~ (Span C,n)) c= BDD (L~ (Span C,n))
A60: (Span C,n) /. (1 + 1) = (Gauge C,n) * ((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) by A1, JORDAN13:def 1;
A61: [(X-SpanStart C,n),(Y-SpanStart C,n)] in Indices (Gauge C,n) by A1, JORDAN11:8;
A62: [((X-SpanStart C,n) -' 1),(Y-SpanStart C,n)] in Indices (Gauge C,n) by A1, JORDAN11:9;
A63: len (Span C,n) >= 1 + 1 by GOBOARD7:36, XXREAL_0:2;
then A64: (right_cell (Span C,n),1,(Gauge C,n)) \ (L~ (Span C,n)) c= RightComp (Span C,n) by A4, JORDAN9:29;
(Span C,n) /. 1 = (Gauge C,n) * (X-SpanStart C,n),(Y-SpanStart C,n) by A1, JORDAN13:def 1;
then right_cell (Span C,n),1,(Gauge C,n) = cell (Gauge C,n),((X-SpanStart C,n) -' 1),(Y-SpanStart C,n) by A4, A8, A63, A60, A61, A62, GOBRD13:27;
hence (cell (Gauge C,n),((X-SpanStart C,n) -' 1),((Y-SpanStart C,n) + 0 )) \ (L~ (Span C,n)) c= BDD (L~ (Span C,n)) by A64, GOBRD14:47; :: thesis: verum
end;
for t being Element of NAT holds S1[t] from NAT_1:sch 1(A59, A10);
 hence (cell (Gauge C,n),((X-SpanStart C,n) -' 1),k) \ (L~ (Span C,n)) c= BDD (L~ (Span C,n)) by A6, A5; :: thesis: verum