let C be Simple_closed_curve; 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; ( 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
; (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;
( 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))) )
;
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 ;
TARSKI:def 3 ( 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)))
;
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;
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))
;
(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)))
;
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 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))
;
contradictionthen 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 )
;
contradictionhence
contradiction
by A7, A8, A26, A17, A33, A34, A36, A38, A40, A45, A47, A46, A30, GOBOARD7:27;
verum end; suppose A48:
(
i1 + 1
= i2 &
j1 = j2 )
;
contradictionthen 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;
verum end; suppose A52:
(
i1 = i2 + 1 &
j1 = j2 )
;
contradictionthen 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;
verum end; suppose
(
i1 = i2 &
j1 = j2 + 1 )
;
contradictionhence
contradiction
by A7, A8, A26, A17, A33, A34, A36, A38, A40, A45, A43, A44, A30, GOBOARD7:27;
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;
verum
end;
A59:
S1[ 0 ]
proof
assume
0 <= (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) - (Y-SpanStart (C,n))
;
(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;
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; verum