let C be Simple_closed_curve; :: thesis: for n, k being 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 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:5;
A5: ro <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n)) by A3, XREAL_1:9;
A6: k = (Y-SpanStart (C,n)) + ro ;
defpred S1[ 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:50;
X-SpanStart (C,n) > 2 by JORDAN1H:49;
then A8: ((X-SpanStart (C,n)) -' 1) + 1 = X-SpanStart (C,n) by XREAL_1:235, XXREAL_0:2;
A9: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by JORDAN1H:50;
A10: for t being Nat st S1[t] holds
S1[t + 1]
proof
let t be 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 object ; :: 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:29; :: 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:69;
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:19;
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:19;
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 object 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))) ;
not x in L~ (Span (C,n)) by A22, XBOOLE_0:def 5;
then x in (L~ (Span (C,n))) ` by A22, SUBSET_1:29;
then x in (BDD (L~ (Span (C,n)))) \/ (UBD (L~ (Span (C,n)))) by JORDAN2C:27;
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:32;
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 :: thesis: not (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))
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:49;
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 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 3;
consider i1, j1, i2, j2 being 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:3;
A40: 1 <= i1 by A35, MATRIX_0:32;
A41: i2 <= len (Gauge (C,n)) by A37, MATRIX_0:32;
A42: 1 <= i2 by A37, MATRIX_0:32;
A43: j1 <= width (Gauge (C,n)) by A35, MATRIX_0:32;
A44: 1 <= j2 by A37, MATRIX_0:32;
A45: i1 <= len (Gauge (C,n)) by A35, MATRIX_0:32;
A46: j2 <= width (Gauge (C,n)) by A37, MATRIX_0:32;
A47: 1 <= j1 by A35, MATRIX_0:32;
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:27; :: 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:26;
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:23;
(X-SpanStart (C,n)) -' 1 = i1 by A7, A8, A26, A17, A33, A34, A36, A38, A40, A47, A43, A41, A30, A48, GOBOARD7:26;
then cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((Y-SpanStart (C,n)) + (t + 1))) meets C by A1, A31, A32, A49, A51, Th7;
hence contradiction by A50, JORDAN1A:7, 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:25;
A54: (Y-SpanStart (C,n)) + (t + 1) = j2 by A7, A8, A26, A17, A33, A34, A36, A38, A45, A47, A43, A42, A30, A52, GOBOARD7:26;
(X-SpanStart (C,n)) -' 1 = i2 by A7, A8, A26, A17, A33, A34, A36, A38, A45, A47, A43, A42, A30, A52, GOBOARD7:26;
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, Th7;
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:7, 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:27; :: 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:21;
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:22;
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:36;
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, Th29, GOBOARD9:4;
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:24; :: 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:34, 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:27;
(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:26;
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:37; :: thesis: verum
end;
for t being Nat holds S1[t] from NAT_1:sch 2(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