let f be non constant standard special_circular_sequence; for k being Nat st 1 <= k & k + 1 <= len f holds
Int (left_cell (f,k)) c= LeftComp f
defpred S1[ Nat] means ( 1 <= $1 & $1 + 1 <= len f implies Int (left_cell (f,$1)) c= LeftComp f );
A1:
S1[ 0 ]
;
A2:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A3:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verumproof
assume that A4:
1
<= k + 1
and A5:
(k + 1) + 1
<= len f
;
Int (left_cell (f,(k + 1))) c= LeftComp f
per cases
( k = 0 or k >= 1 )
by NAT_1:14;
suppose A6:
k >= 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA7:
k + 1
<= len f
by A5, NAT_1:13;
A8:
k <= k + 1
by NAT_1:11;
then
k <= len f
by A7, XXREAL_0:2;
then A9:
k in dom f
by A6, FINSEQ_3:25;
then consider i0,
j0 being
Nat such that A10:
[i0,j0] in Indices (GoB f)
and A11:
f /. k = (GoB f) * (
i0,
j0)
by GOBOARD2:14;
A12:
k + 1
in dom f
by A4, A7, FINSEQ_3:25;
then consider i1,
j1 being
Nat such that A13:
[i1,j1] in Indices (GoB f)
and A14:
f /. (k + 1) = (GoB f) * (
i1,
j1)
by GOBOARD2:14;
(k + 1) + 1
>= 1
by NAT_1:11;
then A15:
(k + 1) + 1
in dom f
by A5, FINSEQ_3:25;
then consider i2,
j2 being
Nat such that A16:
[i2,j2] in Indices (GoB f)
and A17:
f /. ((k + 1) + 1) = (GoB f) * (
i2,
j2)
by GOBOARD2:14;
A18:
1
<= i0
by A10, MATRIX_0:32;
A19:
i0 <= len (GoB f)
by A10, MATRIX_0:32;
A20:
1
<= i1
by A13, MATRIX_0:32;
A21:
i1 <= len (GoB f)
by A13, MATRIX_0:32;
A22:
1
<= i2
by A16, MATRIX_0:32;
A23:
i2 <= len (GoB f)
by A16, MATRIX_0:32;
A24:
1
<= j0
by A10, MATRIX_0:32;
A25:
j0 <= width (GoB f)
by A10, MATRIX_0:32;
A26:
1
<= j1
by A13, MATRIX_0:32;
A27:
j1 <= width (GoB f)
by A13, MATRIX_0:32;
A28:
1
<= j2
by A16, MATRIX_0:32;
A29:
j2 <= width (GoB f)
by A16, MATRIX_0:32;
A30:
(
i0 = i1 or
j0 = j1 )
by A9, A10, A11, A12, A13, A14, GOBOARD2:11;
A31:
(
i1 = i2 or
j1 = j2 )
by A12, A13, A14, A15, A16, A17, GOBOARD2:11;
reconsider i19 =
i1,
i09 =
i0,
i29 =
i2,
j19 =
j1,
j09 =
j0,
j29 =
j2 as
Element of
REAL by XREAL_0:def 1;
A32:
f is_sequence_on GoB f
by GOBOARD5:def 5;
then
|.(i0 - i1).| + |.(j0 - j1).| = 1
by A9, A10, A11, A12, A13, A14;
then A33:
( (
|.(i09 - i19).| = 1 &
j0 = j1 ) or (
|.(j09 - j19).| = 1 &
i0 = i1 ) )
by SEQM_3:42;
then A34:
(
i0 = i1 or
i0 = i1 + 1 or
i0 + 1
= i1 )
by SEQM_3:41;
|.(i1 - i2).| + |.(j1 - j2).| = 1
by A12, A13, A14, A15, A16, A17, A32;
then A35:
( (
|.(i19 - i29).| = 1 &
j1 = j2 ) or (
|.(j19 - j29).| = 1 &
i1 = i2 ) )
by SEQM_3:42;
then A36:
(
i1 = i2 or
i1 = i2 + 1 or
i1 + 1
= i2 )
by SEQM_3:41;
A37:
(
j0 = j1 or
j0 = j1 + 1 or
j0 + 1
= j1 )
by A33, SEQM_3:41;
A38:
(
j1 = j2 or
j1 = j2 + 1 or
j1 + 1
= j2 )
by A35, SEQM_3:41;
A39:
now ( i0 = i2 implies not j0 = j2 )assume that A40:
i0 = i2
and A41:
j0 = j2
;
contradictionA44:
k < (k + 1) + 1
by A8, NAT_1:13;
end;
i1 >= 1
by A13, MATRIX_0:32;
then A45:
i1 = (i1 -' 1) + 1
by XREAL_1:235;
j1 >= 1
by A13, MATRIX_0:32;
then A46:
j1 = (j1 -' 1) + 1
by XREAL_1:235;
then
j1 -' 1
<= j1
by NAT_1:11;
then A47:
j1 -' 1
<= width (GoB f)
by A27, XXREAL_0:2;
len (GoB f) > 1
by GOBOARD7:32;
then A48:
((len (GoB f)) -' 1) + 1
= len (GoB f)
by XREAL_1:235;
width (GoB f) >= 1
by GOBOARD7:33;
then A49:
((width (GoB f)) -' 1) + 1
= width (GoB f)
by XREAL_1:235;
A50:
(k + 1) + 1
= k + (1 + 1)
;
A51:
(i0 + 1) + 1
= i0 + (1 + 1)
;
A52:
(i2 + 1) + 1
= i2 + (1 + 1)
;
A53:
(j0 + 1) + 1
= j0 + (1 + 1)
;
A54:
(j2 + 1) + 1
= j2 + (1 + 1)
;
A55:
LeftComp f is_a_component_of (L~ f) `
by Def1;
A56:
0 + 1
= 1
;
now Int (left_cell (f,(k + 1))) c= LeftComp fper cases
( ( i0 = i1 + 1 & i1 = i2 + 1 & j0 = 1 ) or ( i0 = i1 + 1 & i1 = i2 + 1 & j0 <> 1 ) or ( i0 = i1 + 1 & j1 = j2 + 1 ) or ( j0 = j1 + 1 & i1 = i2 + 1 & i0 = len (GoB f) & j1 = 1 ) or ( j0 = j1 + 1 & i1 = i2 + 1 & i0 <> len (GoB f) & j1 = 1 ) or ( j0 = j1 + 1 & i1 = i2 + 1 & i0 = len (GoB f) & j1 <> 1 ) or ( j0 = j1 + 1 & i1 = i2 + 1 & i0 <> len (GoB f) & j1 <> 1 ) or ( j0 = j1 + 1 & j1 = j2 + 1 & i0 = len (GoB f) ) or ( j0 = j1 + 1 & j1 = j2 + 1 & i0 <> len (GoB f) ) or ( i0 + 1 = i1 & j1 = j2 + 1 & i1 = len (GoB f) & j0 = width (GoB f) ) or ( i0 + 1 = i1 & j1 = j2 + 1 & i1 <> len (GoB f) & j0 = width (GoB f) ) or ( i0 + 1 = i1 & j1 = j2 + 1 & i1 = len (GoB f) & j0 <> width (GoB f) ) or ( i0 + 1 = i1 & j1 = j2 + 1 & i1 <> len (GoB f) & j0 <> width (GoB f) ) or ( j0 + 1 = j1 & i1 = i2 + 1 ) or ( i0 = i1 + 1 & j1 + 1 = j2 & i1 = 1 & j1 = 1 ) or ( i0 = i1 + 1 & j1 + 1 = j2 & i1 <> 1 & j1 = 1 ) or ( i0 = i1 + 1 & j1 + 1 = j2 & i1 = 1 & j1 <> 1 ) or ( i0 = i1 + 1 & j1 + 1 = j2 & i1 <> 1 & j1 <> 1 ) or ( j0 = j1 + 1 & i1 + 1 = i2 ) or ( i0 + 1 = i1 & i1 + 1 = i2 & j0 = width (GoB f) ) or ( i0 + 1 = i1 & i1 + 1 = i2 & j0 <> width (GoB f) ) or ( i0 + 1 = i1 & j1 + 1 = j2 ) or ( j0 + 1 = j1 & i1 + 1 = i2 & i0 = 1 & j1 = width (GoB f) ) or ( j0 + 1 = j1 & i1 + 1 = i2 & i0 <> 1 & j1 = width (GoB f) ) or ( j0 + 1 = j1 & i1 + 1 = i2 & i0 = 1 & j1 <> width (GoB f) ) or ( j0 + 1 = j1 & i1 + 1 = i2 & i0 <> 1 & j1 <> width (GoB f) ) or ( j0 + 1 = j1 & j1 + 1 = j2 & i0 = 1 ) or ( j0 + 1 = j1 & j1 + 1 = j2 & i0 <> 1 ) )
by A9, A11, A12, A14, A15, A17, A34, A36, A37, A38, A39, GOBOARD7:29;
suppose that A57:
i0 = i1 + 1
and A58:
i1 = i2 + 1
and A59:
j0 = 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA60:
left_cell (
f,
k)
= cell (
(GoB f),
i1,
0)
by A6, A7, A10, A11, A13, A14, A30, A56, A57, A59, GOBOARD5:29;
0 + 1
= j2
by A30, A31, A57, A58, A59;
then A61:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i2,
0)
by A4, A5, A13, A14, A16, A17, A30, A57, A58, A59, GOBOARD5:29;
A62:
LSeg (
(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),
(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|))
meets Int (cell ((GoB f),i1,0))
by A19, A20, A57, GOBOARD6:84;
LSeg (
(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),
(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|))
misses L~ f
by A19, A22, A52, A57, A58, GOBOARD8:25;
then
LSeg (
(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),
(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|))
c= (L~ f) `
by SUBSET_1:23;
then A63:
LSeg (
(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),
(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|))
c= LeftComp f
by A3, A5, A6, A55, A60, A62, Th4, NAT_1:13;
A64:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A61, A63, A21, A22, A58, Th4, A64, GOBOARD6:84;
verum end; suppose that A65:
i0 = i1 + 1
and A66:
i1 = i2 + 1
and A67:
j0 <> 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA68:
left_cell (
f,
k)
= cell (
(GoB f),
i1,
(j1 -' 1))
by A6, A7, A10, A11, A13, A14, A30, A46, A65, GOBOARD5:29;
1
< j0
by A24, A67, XXREAL_0:1;
then A69:
1
<= j0 -' 1
by A30, A46, A65, NAT_1:13;
A70:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i2,
(j1 -' 1))
by A4, A5, A13, A14, A16, A17, A31, A46, A66, GOBOARD5:29;
A71:
LSeg (
((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),
((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0)))))
meets Int (cell ((GoB f),i1,(j1 -' 1)))
by A19, A20, A27, A30, A46, A65, A69, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),
((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0)))))
misses L~ f
by A5, A6, A11, A14, A17, A19, A22, A25, A30, A31, A46, A50, A52, A65, A66, A69, GOBOARD8:11;
then
LSeg (
((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),
((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0)))))
c= (L~ f) `
by SUBSET_1:23;
then A72:
LSeg (
((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),
((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0)))))
c= LeftComp f
by A3, A5, A6, A55, A68, A71, Th4, NAT_1:13;
A73:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A30, A55, A65, A66, A70, A72, A21, A22, A25, A46, A69, Th4, A73, GOBOARD6:82;
verum end; suppose that A74:
i0 = i1 + 1
and A75:
j1 = j2 + 1
;
Int (left_cell (f,(k + 1))) c= LeftComp f left_cell (
f,
k) =
cell (
(GoB f),
i1,
j2)
by A6, A7, A10, A11, A13, A14, A30, A74, A75, GOBOARD5:29
.=
left_cell (
f,
(k + 1))
by A4, A5, A13, A14, A16, A17, A31, A45, A75, GOBOARD5:30
;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A3, A5, A6, NAT_1:13;
verum end; suppose that A76:
j0 = j1 + 1
and A77:
i1 = i2 + 1
and A78:
i0 = len (GoB f)
and A79:
j1 = 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA80:
left_cell (
f,
k)
= cell (
(GoB f),
i0,
j1)
by A6, A7, A10, A11, A13, A14, A30, A45, A76, GOBOARD5:30;
A81:
LSeg (
(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|))
meets Int (cell ((GoB f),i0,j1))
by A25, A76, A78, A79, GOBOARD6:86;
LSeg (
(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|))
misses L~ f
by GOBOARD8:35;
then
LSeg (
(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|))
c= (L~ f) `
by SUBSET_1:23;
then A82:
LSeg (
(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|))
c= LeftComp f
by A3, A5, A6, A55, A80, A81, Th4, NAT_1:13;
A83:
Int (cell ((GoB f),i1,0)) is
convex
by A21, A26, A27, Th16;
Int (cell ((GoB f),i1,0)) misses L~ f
by A21, A26, A27, GOBOARD7:12;
then
Int (cell ((GoB f),i1,0)) c= (L~ f) `
by SUBSET_1:23;
then A84:
Int (cell ((GoB f),i1,0)) c= LeftComp f
by A55, A82, A30, A76, A78, Th4, A83, GOBOARD6:90;
A85:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i2,
0)
by A4, A5, A13, A14, A16, A17, A31, A46, A77, A79, GOBOARD5:29;
A86:
LSeg (
(((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),
(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|))
meets Int (cell ((GoB f),i1,0))
by A30, A76, A78, GOBOARD6:90;
LSeg (
(((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),
(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|))
misses L~ f
by GOBOARD8:27;
then
LSeg (
(((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),
(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|))
c= (L~ f) `
by SUBSET_1:23;
then A87:
LSeg (
(((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),
(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|))
c= LeftComp f
by A55, A84, A86, Th4;
A88:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A85, A87, A22, A30, A45, A76, A77, A78, Th4, A88, GOBOARD6:84;
verum end; suppose that A89:
j0 = j1 + 1
and A90:
i1 = i2 + 1
and A91:
i0 <> len (GoB f)
and A92:
j1 = 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA93:
left_cell (
f,
k)
= cell (
(GoB f),
i0,
j1)
by A6, A7, A10, A11, A13, A14, A30, A45, A89, GOBOARD5:30;
len (GoB f) > i0
by A19, A91, XXREAL_0:1;
then A94:
len (GoB f) >= i0 + 1
by NAT_1:13;
A95:
LSeg (
(((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),
((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),(1 + 1))))))
meets Int (cell ((GoB f),i0,j1))
by A20, A25, A30, A89, A92, A94, GOBOARD6:82;
LSeg (
(((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),
((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2)))))
misses L~ f
by A5, A6, A11, A14, A17, A22, A30, A31, A50, A52, A89, A90, A92, A94, GOBOARD8:8;
then
LSeg (
(((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),
((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2)))))
c= (L~ f) `
by SUBSET_1:23;
then A96:
LSeg (
(((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),
((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2)))))
c= LeftComp f
by A3, A5, A6, A55, A93, A95, Th4, NAT_1:13;
A97:
Int (cell ((GoB f),i1,0)) is
convex
by A21, A26, A27, Th16;
Int (cell ((GoB f),i1,0)) misses L~ f
by A21, A26, A27, GOBOARD7:12;
then
Int (cell ((GoB f),i1,0)) c= (L~ f) `
by SUBSET_1:23;
then A98:
Int (cell ((GoB f),i1,0)) c= LeftComp f
by A55, A96, A20, A30, A89, A94, Th4, A97, GOBOARD6:84;
A99:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i2,
0)
by A4, A5, A13, A14, A16, A17, A31, A46, A90, A92, GOBOARD5:29;
A100:
LSeg (
(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),
(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|))
meets Int (cell ((GoB f),i1,0))
by A20, A30, A89, A90, A94, GOBOARD6:84;
LSeg (
(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),
(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|))
misses L~ f
by A22, A30, A89, A90, A94, GOBOARD8:25;
then
LSeg (
(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),
(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|))
c= (L~ f) `
by SUBSET_1:23;
then A101:
LSeg (
(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),
(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|))
c= LeftComp f
by A55, A98, A100, Th4;
A102:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A99, A101, A21, A22, A90, Th4, A102, GOBOARD6:84;
verum end; suppose that A103:
j0 = j1 + 1
and A104:
i1 = i2 + 1
and A105:
i0 = len (GoB f)
and A106:
j1 <> 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA107:
left_cell (
f,
k)
= cell (
(GoB f),
i0,
j1)
by A6, A7, A10, A11, A13, A14, A30, A45, A103, GOBOARD5:30;
1
< j1
by A26, A106, XXREAL_0:1;
then A108:
1
<= j1 -' 1
by A46, NAT_1:13;
A109:
j1 + 1
= (j1 -' 1) + (1 + 1)
by A46;
A110:
LSeg (
(((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|))
meets Int (cell ((GoB f),i0,j1))
by A25, A26, A103, A105, GOBOARD6:86;
LSeg (
(((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|))
misses L~ f
by A25, A46, A103, A108, A109, GOBOARD8:34;
then
LSeg (
(((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|))
c= (L~ f) `
by SUBSET_1:23;
then A111:
LSeg (
(((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|))
c= LeftComp f
by A3, A5, A6, A55, A107, A110, Th4, NAT_1:13;
j1 > 1
by A26, A106, XXREAL_0:1;
then A112:
1
<= j1 -' 1
by A46, NAT_1:13;
A113:
Int (cell ((GoB f),i1,(j1 -' 1))) is
convex
by A21, A47, Th16;
Int (cell ((GoB f),i1,(j1 -' 1))) misses L~ f
by A21, A47, GOBOARD7:12;
then
Int (cell ((GoB f),i1,(j1 -' 1))) c= (L~ f) `
by SUBSET_1:23;
then A114:
Int (cell ((GoB f),i1,(j1 -' 1))) c= LeftComp f
by A55, A111, A27, A30, A46, A103, A105, Th4, A113, A112, GOBOARD6:86;
A115:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i2,
(j1 -' 1))
by A4, A5, A13, A14, A16, A17, A31, A46, A104, GOBOARD5:29;
A116:
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),
(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|))
meets Int (cell ((GoB f),i1,(j1 -' 1)))
by A27, A30, A46, A103, A105, A108, GOBOARD6:86;
A117:
i1 -' 1
= i2
by A104, NAT_D:34;
then
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),
(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|))
misses L~ f
by A5, A6, A11, A14, A17, A25, A30, A31, A46, A50, A103, A104, A105, A108, A109, GOBOARD8:19;
then
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),
(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|))
c= (L~ f) `
by SUBSET_1:23;
then A118:
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),
(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|))
c= LeftComp f
by A55, A114, A116, Th4;
A119:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A115, A118, A21, A22, A27, A46, A104, A108, A117, Th4, A119, GOBOARD6:82;
verum end; suppose that A120:
j0 = j1 + 1
and A121:
i1 = i2 + 1
and A122:
i0 <> len (GoB f)
and A123:
j1 <> 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA124:
left_cell (
f,
k)
= cell (
(GoB f),
i0,
j1)
by A6, A7, A10, A11, A13, A14, A30, A45, A120, GOBOARD5:30;
1
< j1
by A26, A123, XXREAL_0:1;
then A125:
1
<= j1 -' 1
by A46, NAT_1:13;
len (GoB f) > i0
by A19, A122, XXREAL_0:1;
then A126:
len (GoB f) >= i0 + 1
by NAT_1:13;
A127:
j1 + 1
= (j1 -' 1) + (1 + 1)
by A46;
A128:
LSeg (
((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),
((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1))))))
meets Int (cell ((GoB f),i0,j1))
by A20, A25, A26, A30, A120, A126, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),
((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1))))))
misses L~ f
by A5, A6, A11, A14, A17, A22, A25, A30, A31, A46, A50, A52, A120, A121, A125, A126, A127, GOBOARD8:5;
then
LSeg (
((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),
((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1))))))
c= (L~ f) `
by SUBSET_1:23;
then A129:
LSeg (
((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),
((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1))))))
c= LeftComp f
by A3, A5, A6, A55, A124, A128, Th4, NAT_1:13;
j1 > 1
by A26, A123, XXREAL_0:1;
then A130:
1
<= j1 -' 1
by A46, NAT_1:13;
A131:
Int (cell ((GoB f),i1,(j1 -' 1))) is
convex
by A21, A47, Th16;
Int (cell ((GoB f),i1,(j1 -' 1))) misses L~ f
by A21, A47, GOBOARD7:12;
then
Int (cell ((GoB f),i1,(j1 -' 1))) c= (L~ f) `
by SUBSET_1:23;
then A132:
Int (cell ((GoB f),i1,(j1 -' 1))) c= LeftComp f
by A30, A55, A120, A129, A20, A27, A46, A126, Th4, A131, A130, GOBOARD6:82;
A133:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i2,
(j1 -' 1))
by A4, A5, A13, A14, A16, A17, A31, A46, A121, GOBOARD5:29;
A134:
LSeg (
((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),
((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1)))))
meets Int (cell ((GoB f),i1,(j1 -' 1)))
by A20, A27, A30, A46, A120, A125, A126, GOBOARD6:82;
i1 < len (GoB f)
by A21, A30, A120, A122, XXREAL_0:1;
then
i1 + 1
<= len (GoB f)
by NAT_1:13;
then
LSeg (
((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),
((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1)))))
misses L~ f
by A5, A6, A11, A14, A17, A22, A25, A30, A31, A46, A50, A52, A120, A121, A125, A127, GOBOARD8:13;
then
LSeg (
((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),
((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1)))))
c= (L~ f) `
by SUBSET_1:23;
then A135:
LSeg (
((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),
((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1)))))
c= LeftComp f
by A55, A132, A134, Th4;
A136:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A121, A133, A135, A21, A22, A27, A46, A125, Th4, A136, GOBOARD6:82;
verum end; suppose that A137:
j0 = j1 + 1
and A138:
j1 = j2 + 1
and A139:
i0 = len (GoB f)
;
Int (left_cell (f,(k + 1))) c= LeftComp fA140:
left_cell (
f,
k)
= cell (
(GoB f),
(len (GoB f)),
j1)
by A6, A7, A10, A11, A13, A14, A30, A48, A137, A139, GOBOARD5:30;
A141:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
(len (GoB f)),
j2)
by A4, A5, A13, A14, A16, A17, A30, A31, A48, A137, A138, A139, GOBOARD5:30;
A142:
LSeg (
(((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|))
meets Int (cell ((GoB f),(len (GoB f)),j1))
by A25, A26, A137, A138, GOBOARD6:86;
LSeg (
(((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|))
misses L~ f
by A25, A28, A137, A138, GOBOARD8:34;
then
LSeg (
(((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|))
c= (L~ f) `
by SUBSET_1:23;
then A143:
LSeg (
(((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|))
c= LeftComp f
by A3, A5, A6, A55, A140, A142, Th4, NAT_1:13;
A144:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A141, A143, A27, A28, A138, Th4, A144, GOBOARD6:86;
verum end; suppose that A145:
j0 = j1 + 1
and A146:
j1 = j2 + 1
and A147:
i0 <> len (GoB f)
;
Int (left_cell (f,(k + 1))) c= LeftComp fA148:
left_cell (
f,
k)
= cell (
(GoB f),
i0,
j1)
by A6, A7, A10, A11, A13, A14, A30, A45, A145, GOBOARD5:30;
len (GoB f) > i0
by A19, A147, XXREAL_0:1;
then A149:
len (GoB f) >= i0 + 1
by NAT_1:13;
A150:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i1,
j2)
by A4, A5, A13, A14, A16, A17, A31, A45, A146, GOBOARD5:30;
A151:
LSeg (
((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),
((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2))))))
meets Int (cell ((GoB f),i0,j1))
by A20, A25, A26, A30, A145, A146, A149, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),
((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2))))))
misses L~ f
by A5, A6, A11, A14, A17, A18, A25, A28, A30, A31, A50, A145, A146, A149, GOBOARD8:4;
then
LSeg (
((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),
((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2))))))
c= (L~ f) `
by SUBSET_1:23;
then A152:
LSeg (
((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),
((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2))))))
c= LeftComp f
by A3, A5, A6, A55, A148, A151, Th4, NAT_1:13;
A153:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A150, A152, A20, A27, A28, A30, A145, A146, A149, Th4, A153, GOBOARD6:82;
verum end; suppose that A154:
i0 + 1
= i1
and A155:
j1 = j2 + 1
and A156:
i1 = len (GoB f)
and A157:
j0 = width (GoB f)
;
Int (left_cell (f,(k + 1))) c= LeftComp fA158:
left_cell (
f,
k)
= cell (
(GoB f),
i0,
j1)
by A6, A7, A10, A11, A13, A14, A30, A46, A154, GOBOARD5:28;
A159:
LSeg (
(((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),
(((GoB f) * (i1,j0)) + |[1,1]|))
meets Int (cell ((GoB f),i0,j1))
by A18, A21, A30, A154, A157, GOBOARD6:83;
LSeg (
(((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),
(((GoB f) * (i1,j0)) + |[1,1]|))
misses L~ f
by A48, A154, A156, A157, GOBOARD8:30;
then
LSeg (
(((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),
(((GoB f) * (i1,j0)) + |[1,1]|))
c= (L~ f) `
by SUBSET_1:23;
then A160:
LSeg (
(((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),
(((GoB f) * (i1,j0)) + |[1,1]|))
c= LeftComp f
by A3, A5, A6, A55, A158, A159, Th4, NAT_1:13;
A161:
Int (cell ((GoB f),i1,j1)) is
convex
by A21, A27, Th16;
Int (cell ((GoB f),i1,j1)) misses L~ f
by A21, A27, GOBOARD7:12;
then
Int (cell ((GoB f),i1,j1)) c= (L~ f) `
by SUBSET_1:23;
then A162:
Int (cell ((GoB f),i1,j1)) c= LeftComp f
by A55, A160, A30, A154, A156, A157, Th4, A161, GOBOARD6:88;
A163:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i1,
j2)
by A4, A5, A13, A14, A16, A17, A31, A45, A155, GOBOARD5:30;
A164:
LSeg (
(((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),
(((GoB f) * (i1,j1)) + |[1,1]|))
meets Int (cell ((GoB f),i1,j1))
by A30, A154, A156, A157, GOBOARD6:88;
LSeg (
(((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),
(((GoB f) * (i1,j1)) + |[1,1]|))
misses L~ f
by A30, A49, A154, A155, A156, A157, GOBOARD8:36;
then
LSeg (
(((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),
(((GoB f) * (i1,j1)) + |[1,1]|))
c= (L~ f) `
by SUBSET_1:23;
then A165:
LSeg (
(((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),
(((GoB f) * (i1,j1)) + |[1,1]|))
c= LeftComp f
by A55, A162, A164, Th4;
A166:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A163, A165, A27, A28, A155, A156, Th4, A166, GOBOARD6:86;
verum end; suppose that A167:
i0 + 1
= i1
and A168:
j1 = j2 + 1
and A169:
i1 <> len (GoB f)
and A170:
j0 = width (GoB f)
;
Int (left_cell (f,(k + 1))) c= LeftComp fA171:
left_cell (
f,
k)
= cell (
(GoB f),
i0,
j1)
by A6, A7, A10, A11, A13, A14, A30, A46, A167, GOBOARD5:28;
len (GoB f) > i1
by A21, A169, XXREAL_0:1;
then A172:
i1 + 1
<= len (GoB f)
by NAT_1:13;
A173:
LSeg (
(((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),
(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|))
meets Int (cell ((GoB f),i0,j1))
by A18, A21, A30, A167, A170, GOBOARD6:83;
LSeg (
(((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),
(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|))
misses L~ f
by A18, A167, A170, A172, GOBOARD8:28;
then
LSeg (
(((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),
(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|))
c= (L~ f) `
by SUBSET_1:23;
then A174:
LSeg (
(((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),
(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|))
c= LeftComp f
by A3, A5, A6, A55, A171, A173, Th4, NAT_1:13;
A175:
Int (cell ((GoB f),i1,j1)) is
convex
by A21, A27, Th16;
Int (cell ((GoB f),i1,j1)) misses L~ f
by A21, A27, GOBOARD7:12;
then
Int (cell ((GoB f),i1,j1)) c= (L~ f) `
by SUBSET_1:23;
then A176:
Int (cell ((GoB f),i1,j1)) c= LeftComp f
by A55, A174, A20, A30, A167, A170, A172, Th4, A175, GOBOARD6:83;
A177:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i1,
j2)
by A4, A5, A13, A14, A16, A17, A31, A45, A168, GOBOARD5:30;
A178:
LSeg (
((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),
(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|))
meets Int (cell ((GoB f),i1,j1))
by A20, A30, A167, A170, A172, GOBOARD6:83;
LSeg (
((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),
(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|))
misses L~ f
by A5, A6, A11, A14, A17, A18, A30, A31, A49, A50, A51, A167, A168, A170, A172, GOBOARD8:10;
then
LSeg (
((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),
(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|))
c= (L~ f) `
by SUBSET_1:23;
then A179:
LSeg (
((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),
(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|))
c= LeftComp f
by A55, A176, A178, Th4;
A180:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A177, A179, A20, A28, A30, A167, A168, A170, A172, Th4, A180, GOBOARD6:82;
verum end; suppose that A181:
i0 + 1
= i1
and A182:
j1 = j2 + 1
and A183:
i1 = len (GoB f)
and A184:
j0 <> width (GoB f)
;
Int (left_cell (f,(k + 1))) c= LeftComp fA185:
left_cell (
f,
k)
= cell (
(GoB f),
i0,
j1)
by A6, A7, A10, A11, A13, A14, A30, A46, A181, GOBOARD5:28;
width (GoB f) > j0
by A25, A184, XXREAL_0:1;
then A186:
width (GoB f) >= j0 + 1
by NAT_1:13;
A187:
LSeg (
((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|))
meets Int (cell ((GoB f),i0,j1))
by A18, A21, A26, A30, A181, A186, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|))
misses L~ f
by A5, A6, A11, A14, A17, A28, A30, A31, A48, A50, A54, A181, A182, A183, A186, GOBOARD8:20;
then
LSeg (
((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|))
c= (L~ f) `
by SUBSET_1:23;
then A188:
LSeg (
((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|))
c= LeftComp f
by A3, A5, A6, A55, A185, A187, Th4, NAT_1:13;
A189:
Int (cell ((GoB f),i1,j1)) is
convex
by A21, A27, Th16;
Int (cell ((GoB f),i1,j1)) misses L~ f
by A21, A27, GOBOARD7:12;
then
Int (cell ((GoB f),i1,j1)) c= (L~ f) `
by SUBSET_1:23;
then A190:
Int (cell ((GoB f),i1,j1)) c= LeftComp f
by A55, A188, A26, A30, A181, A183, A186, Th4, A189, GOBOARD6:86;
A191:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i1,
j2)
by A4, A5, A13, A14, A16, A17, A31, A45, A182, GOBOARD5:30;
A192:
LSeg (
(((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|))
meets Int (cell ((GoB f),i1,j1))
by A26, A30, A181, A183, A186, GOBOARD6:86;
LSeg (
(((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|))
misses L~ f
by A28, A30, A54, A181, A182, A186, GOBOARD8:34;
then
LSeg (
(((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|))
c= (L~ f) `
by SUBSET_1:23;
then A193:
LSeg (
(((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),
(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|))
c= LeftComp f
by A55, A190, A192, Th4;
A194:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A191, A193, A27, A28, A182, A183, Th4, A194, GOBOARD6:86;
verum end; suppose that A195:
i0 + 1
= i1
and A196:
j1 = j2 + 1
and A197:
i1 <> len (GoB f)
and A198:
j0 <> width (GoB f)
;
Int (left_cell (f,(k + 1))) c= LeftComp fA199:
left_cell (
f,
k)
= cell (
(GoB f),
i0,
j1)
by A6, A7, A10, A11, A13, A14, A30, A46, A195, GOBOARD5:28;
len (GoB f) > i1
by A21, A197, XXREAL_0:1;
then A200:
i1 + 1
<= len (GoB f)
by NAT_1:13;
width (GoB f) > j0
by A25, A198, XXREAL_0:1;
then A201:
width (GoB f) >= j0 + 1
by NAT_1:13;
A202:
LSeg (
((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),
((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1))))))
meets Int (cell ((GoB f),i0,j1))
by A18, A21, A26, A30, A195, A196, A201, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),
((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1))))))
misses L~ f
by A5, A6, A11, A14, A17, A18, A28, A30, A31, A50, A51, A54, A195, A196, A200, A201, GOBOARD8:16;
then
LSeg (
((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),
((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1))))))
c= (L~ f) `
by SUBSET_1:23;
then A203:
LSeg (
((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),
((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1))))))
c= LeftComp f
by A3, A5, A6, A55, A199, A202, Th4, NAT_1:13;
A204:
Int (cell ((GoB f),i1,j1)) is
convex
by A21, A27, Th16;
Int (cell ((GoB f),i1,j1)) misses L~ f
by A21, A27, GOBOARD7:12;
then
Int (cell ((GoB f),i1,j1)) c= (L~ f) `
by SUBSET_1:23;
then A205:
Int (cell ((GoB f),i1,j1)) c= LeftComp f
by A55, A203, A20, A26, A30, A195, A196, A200, A201, Th4, A204, GOBOARD6:82;
A206:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i1,
j2)
by A4, A5, A13, A14, A16, A17, A31, A45, A196, GOBOARD5:30;
A207:
LSeg (
((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),
((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1))))))
meets Int (cell ((GoB f),i1,j1))
by A20, A26, A30, A195, A196, A200, A201, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),
((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1))))))
misses L~ f
by A5, A6, A11, A14, A17, A18, A28, A30, A31, A50, A51, A54, A195, A196, A200, A201, GOBOARD8:6;
then
LSeg (
((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),
((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1))))))
c= (L~ f) `
by SUBSET_1:23;
then A208:
LSeg (
((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),
((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1))))))
c= LeftComp f
by A55, A205, A207, Th4;
A209:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A206, A208, A20, A27, A28, A195, A196, A200, Th4, A209, GOBOARD6:82;
verum end; suppose that A210:
j0 + 1
= j1
and A211:
i1 = i2 + 1
;
Int (left_cell (f,(k + 1))) c= LeftComp f left_cell (
f,
k) =
cell (
(GoB f),
i2,
j0)
by A6, A7, A10, A11, A13, A14, A30, A210, A211, GOBOARD5:27
.=
left_cell (
f,
(k + 1))
by A4, A5, A13, A14, A16, A17, A31, A210, A211, GOBOARD5:29
;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A3, A5, A6, NAT_1:13;
verum end; suppose that A212:
i0 = i1 + 1
and A213:
j1 + 1
= j2
and A214:
i1 = 1
and A215:
j1 = 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA216:
left_cell (
f,
k)
= cell (
(GoB f),
i1,
(j1 -' 1))
by A6, A7, A10, A11, A13, A14, A30, A46, A212, GOBOARD5:29;
i1 -' 1
<= i1
by NAT_D:35;
then A217:
i1 -' 1
<= len (GoB f)
by A21, XXREAL_0:2;
A218:
j1 -' 1
= 0
by A215, XREAL_1:232;
A219:
i1 -' 1
= 0
by A214, XREAL_1:232;
j1 -' 1
<= j1
by NAT_D:35;
then A220:
j1 -' 1
<= width (GoB f)
by A27, XXREAL_0:2;
A221:
LSeg (
(((GoB f) * (i1,j1)) - |[1,1]|),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|))
meets Int (cell ((GoB f),i1,(j1 -' 1)))
by A19, A20, A212, A215, A218, GOBOARD6:84;
LSeg (
(((GoB f) * (i1,j1)) - |[1,1]|),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|))
misses L~ f
by A212, A214, A215, GOBOARD8:26;
then
LSeg (
(((GoB f) * (i1,j1)) - |[1,1]|),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|))
c= (L~ f) `
by SUBSET_1:23;
then A222:
LSeg (
(((GoB f) * (i1,j1)) - |[1,1]|),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|))
c= LeftComp f
by A3, A5, A6, A55, A216, A221, Th4, NAT_1:13;
A223:
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is
convex
by A217, A220, Th16;
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f
by A217, A220, GOBOARD7:12;
then
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) `
by SUBSET_1:23;
then A224:
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f
by A55, A222, A214, A215, A218, Th4, A223, GOBOARD6:87;
A225:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
(i1 -' 1),
j1)
by A4, A5, A13, A14, A16, A17, A31, A45, A213, GOBOARD5:27;
A226:
LSeg (
(((GoB f) * (i1,j1)) - |[1,1]|),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|))
meets Int (cell ((GoB f),(i1 -' 1),(j1 -' 1)))
by A214, A215, A218, GOBOARD6:87;
LSeg (
(((GoB f) * (i1,j1)) - |[1,1]|),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|))
misses L~ f
by A213, A214, A215, GOBOARD8:32;
then
LSeg (
(((GoB f) * (i1,j1)) - |[1,1]|),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|))
c= (L~ f) `
by SUBSET_1:23;
then A227:
LSeg (
(((GoB f) * (i1,j1)) - |[1,1]|),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|))
c= LeftComp f
by A55, A224, A226, Th4;
A228:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A225, A227, A26, A29, A213, A214, A219, Th4, A228, GOBOARD6:85;
verum end; suppose that A229:
i0 = i1 + 1
and A230:
j1 + 1
= j2
and A231:
i1 <> 1
and A232:
j1 = 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA233:
left_cell (
f,
k)
= cell (
(GoB f),
i1,
(j1 -' 1))
by A6, A7, A10, A11, A13, A14, A30, A46, A229, GOBOARD5:29;
1
< i1
by A20, A231, XXREAL_0:1;
then A234:
1
<= i1 -' 1
by A45, NAT_1:13;
A235:
(i1 -' 1) + (1 + 1) = i0
by A45, A229;
i1 -' 1
<= i1
by NAT_D:35;
then A236:
i1 -' 1
<= len (GoB f)
by A21, XXREAL_0:2;
A237:
j1 -' 1
= 0
by A232, XREAL_1:232;
j1 -' 1
<= j1
by NAT_D:35;
then A238:
j1 -' 1
<= width (GoB f)
by A27, XXREAL_0:2;
A239:
LSeg (
(((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),
(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|))
meets Int (cell ((GoB f),i1,(j1 -' 1)))
by A19, A20, A229, A237, GOBOARD6:84;
LSeg (
(((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),
(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|))
misses L~ f
by A19, A45, A234, A235, GOBOARD8:25;
then
LSeg (
(((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),
(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|))
c= (L~ f) `
by SUBSET_1:23;
then A240:
LSeg (
(((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),
(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|))
c= LeftComp f
by A3, A5, A6, A55, A233, A239, Th4, NAT_1:13;
A241:
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is
convex
by A236, A238, Th16;
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f
by A236, A238, GOBOARD7:12;
then
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) `
by SUBSET_1:23;
then A242:
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f
by A55, A240, A21, A45, A234, A237, Th4, A241, GOBOARD6:84;
A243:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
(i1 -' 1),
j1)
by A4, A5, A13, A14, A16, A17, A31, A45, A230, GOBOARD5:27;
A244:
LSeg (
(((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),
((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2)))))
meets Int (cell ((GoB f),(i1 -' 1),(j1 -' 1)))
by A21, A45, A234, A237, GOBOARD6:84;
LSeg (
(((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),
((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2)))))
misses L~ f
by A5, A6, A11, A14, A17, A19, A30, A31, A45, A50, A230, A232, A234, A235, GOBOARD8:7;
then
LSeg (
(((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),
((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2)))))
c= (L~ f) `
by SUBSET_1:23;
then A245:
LSeg (
(((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),
((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2)))))
c= LeftComp f
by A55, A242, A244, Th4;
A246:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A243, A245, A21, A29, A45, A230, A232, A234, Th4, A246, GOBOARD6:82;
verum end; suppose that A247:
i0 = i1 + 1
and A248:
j1 + 1
= j2
and A249:
i1 = 1
and A250:
j1 <> 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA251:
left_cell (
f,
k)
= cell (
(GoB f),
i1,
(j1 -' 1))
by A6, A7, A10, A11, A13, A14, A30, A46, A247, GOBOARD5:29;
1
< j0
by A24, A30, A247, A250, XXREAL_0:1;
then A252:
1
<= j0 -' 1
by A30, A46, A247, NAT_1:13;
A253:
(j0 -' 1) + (1 + 1) = j2
by A30, A46, A247, A248;
A254:
LSeg (
(((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),
((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1))))))
meets Int (cell ((GoB f),i1,(j1 -' 1)))
by A19, A27, A30, A46, A247, A249, A252, GOBOARD6:82;
LSeg (
(((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),
((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1))))))
misses L~ f
by A5, A6, A11, A14, A17, A29, A30, A31, A46, A50, A247, A248, A249, A252, A253, GOBOARD8:17;
then
LSeg (
(((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),
((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1))))))
c= (L~ f) `
by SUBSET_1:23;
then A255:
LSeg (
(((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),
((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1))))))
c= LeftComp f
by A3, A5, A6, A55, A251, A254, Th4, NAT_1:13;
i1 -' 1
<= i1
by NAT_D:35;
then A256:
i1 -' 1
<= len (GoB f)
by A21, XXREAL_0:2;
A257:
i1 -' 1
= 0
by A249, XREAL_1:232;
j1 -' 1
<= j1
by NAT_D:35;
then A258:
j1 -' 1
<= width (GoB f)
by A27, XXREAL_0:2;
A259:
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is
convex
by A256, A258, Th16;
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f
by A256, A258, GOBOARD7:12;
then
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) `
by SUBSET_1:23;
then A260:
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f
by A30, A55, A247, A255, A27, A46, A252, A257, Th4, A259, GOBOARD6:85;
A261:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
(i1 -' 1),
j1)
by A4, A5, A13, A14, A16, A17, A31, A45, A248, GOBOARD5:27;
A262:
LSeg (
(((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),
(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|))
meets Int (cell ((GoB f),(i1 -' 1),(j1 -' 1)))
by A27, A30, A46, A247, A252, A257, GOBOARD6:85;
LSeg (
(((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),
(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|))
misses L~ f
by A29, A30, A46, A247, A248, A252, GOBOARD8:31;
then
LSeg (
(((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),
(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|))
c= (L~ f) `
by SUBSET_1:23;
then A263:
LSeg (
(((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),
(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|))
c= LeftComp f
by A55, A260, A262, Th4;
A264:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A261, A263, A26, A29, A46, A248, A257, Th4, A264, GOBOARD6:85;
verum end; suppose that A265:
i0 = i1 + 1
and A266:
j1 + 1
= j2
and A267:
i1 <> 1
and A268:
j1 <> 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA269:
left_cell (
f,
k)
= cell (
(GoB f),
i1,
(j1 -' 1))
by A6, A7, A10, A11, A13, A14, A30, A46, A265, GOBOARD5:29;
1
< j0
by A24, A30, A265, A268, XXREAL_0:1;
then A270:
1
<= j0 -' 1
by A30, A46, A265, NAT_1:13;
1
< i1
by A20, A267, XXREAL_0:1;
then A271:
1
<= i1 -' 1
by A45, NAT_1:13;
A272:
(i1 -' 1) + (1 + 1) = i0
by A45, A265;
A273:
(j0 -' 1) + (1 + 1) = j2
by A30, A46, A265, A266;
A274:
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),
((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1)))))
meets Int (cell ((GoB f),i1,(j1 -' 1)))
by A19, A20, A27, A30, A46, A265, A270, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),
((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1)))))
misses L~ f
by A5, A6, A11, A14, A17, A19, A29, A30, A31, A45, A46, A50, A266, A270, A271, A272, A273, GOBOARD8:12;
then
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),
((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1)))))
c= (L~ f) `
by SUBSET_1:23;
then A275:
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),
((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1)))))
c= LeftComp f
by A3, A5, A6, A55, A269, A274, Th4, NAT_1:13;
i1 -' 1
<= i1
by NAT_D:35;
then A276:
i1 -' 1
<= len (GoB f)
by A21, XXREAL_0:2;
j1 -' 1
<= j1
by NAT_D:35;
then A277:
j1 -' 1
<= width (GoB f)
by A27, XXREAL_0:2;
A278:
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is
convex
by A276, A277, Th16;
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f
by A276, A277, GOBOARD7:12;
then
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) `
by SUBSET_1:23;
then A279:
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f
by A30, A55, A265, A275, A21, A27, A45, A46, A270, A271, Th4, A278, GOBOARD6:82;
A280:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
(i1 -' 1),
j1)
by A4, A5, A13, A14, A16, A17, A31, A45, A266, GOBOARD5:27;
A281:
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),
((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2)))))
meets Int (cell ((GoB f),(i1 -' 1),(j1 -' 1)))
by A21, A27, A30, A45, A46, A265, A270, A271, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),
((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2)))))
misses L~ f
by A5, A6, A11, A14, A17, A19, A29, A30, A31, A45, A46, A50, A266, A270, A271, A272, A273, GOBOARD8:2;
then
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),
((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2)))))
c= (L~ f) `
by SUBSET_1:23;
then A282:
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),
((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2)))))
c= LeftComp f
by A55, A279, A281, Th4;
A283:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A280, A282, A21, A26, A29, A45, A266, A271, Th4, A283, GOBOARD6:82;
verum end; suppose that A284:
j0 = j1 + 1
and A285:
i1 + 1
= i2
;
Int (left_cell (f,(k + 1))) c= LeftComp f left_cell (
f,
k) =
cell (
(GoB f),
i0,
j1)
by A6, A7, A10, A11, A13, A14, A30, A45, A284, GOBOARD5:30
.=
left_cell (
f,
(k + 1))
by A4, A5, A13, A14, A16, A17, A30, A31, A46, A284, A285, GOBOARD5:28
;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A3, A5, A6, NAT_1:13;
verum end; suppose that A286:
i0 + 1
= i1
and A287:
i1 + 1
= i2
and A288:
j0 = width (GoB f)
;
Int (left_cell (f,(k + 1))) c= LeftComp fA289:
left_cell (
f,
k)
= cell (
(GoB f),
i0,
(width (GoB f)))
by A6, A7, A10, A11, A13, A14, A30, A49, A286, A288, GOBOARD5:28;
A290:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i1,
(width (GoB f)))
by A4, A5, A13, A14, A16, A17, A30, A31, A49, A286, A287, A288, GOBOARD5:28;
A291:
LSeg (
(((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),
(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|))
meets Int (cell ((GoB f),i0,(width (GoB f))))
by A18, A21, A286, GOBOARD6:83;
LSeg (
(((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),
(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|))
misses L~ f
by A18, A23, A51, A286, A287, GOBOARD8:28;
then
LSeg (
(((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),
(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|))
c= (L~ f) `
by SUBSET_1:23;
then A292:
LSeg (
(((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),
(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|))
c= LeftComp f
by A3, A5, A6, A55, A289, A291, Th4, NAT_1:13;
A293:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A290, A292, A20, A23, A287, Th4, A293, GOBOARD6:83;
verum end; suppose that A294:
i0 + 1
= i1
and A295:
i1 + 1
= i2
and A296:
j0 <> width (GoB f)
;
Int (left_cell (f,(k + 1))) c= LeftComp fA297:
left_cell (
f,
k)
= cell (
(GoB f),
i0,
j1)
by A6, A7, A10, A11, A13, A14, A30, A46, A294, GOBOARD5:28;
width (GoB f) > j0
by A25, A296, XXREAL_0:1;
then A298:
width (GoB f) >= j0 + 1
by NAT_1:13;
A299:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i1,
j1)
by A4, A5, A13, A14, A16, A17, A31, A46, A295, GOBOARD5:28;
A300:
LSeg (
((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),
((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1))))))
meets Int (cell ((GoB f),i0,j1))
by A18, A21, A26, A30, A294, A298, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),
((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1))))))
misses L~ f
by A5, A6, A11, A14, A17, A18, A23, A24, A30, A31, A50, A51, A294, A295, A298, GOBOARD8:14;
then
LSeg (
((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),
((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1))))))
c= (L~ f) `
by SUBSET_1:23;
then A301:
LSeg (
((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),
((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1))))))
c= LeftComp f
by A3, A5, A6, A55, A297, A300, Th4, NAT_1:13;
A302:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A299, A301, A20, A23, A24, A30, A294, A295, A298, Th4, A302, GOBOARD6:82;
verum end; suppose that A303:
i0 + 1
= i1
and A304:
j1 + 1
= j2
;
Int (left_cell (f,(k + 1))) c= LeftComp f left_cell (
f,
k) =
cell (
(GoB f),
i0,
j1)
by A6, A7, A10, A11, A13, A14, A30, A46, A303, GOBOARD5:28
.=
left_cell (
f,
(k + 1))
by A4, A5, A13, A14, A16, A17, A31, A303, A304, GOBOARD5:27
;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A3, A5, A6, NAT_1:13;
verum end; suppose that A305:
j0 + 1
= j1
and A306:
i1 + 1
= i2
and A307:
i0 = 1
and A308:
j1 = width (GoB f)
;
Int (left_cell (f,(k + 1))) c= LeftComp fA309:
left_cell (
f,
k)
= cell (
(GoB f),
(i1 -' 1),
j0)
by A6, A7, A10, A11, A13, A14, A30, A45, A305, GOBOARD5:27;
A310:
i0 -' 1
= 0
by A307, XREAL_1:232;
A311:
j1 -' 1
= j0
by A305, NAT_D:34;
A312:
LSeg (
(((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),
(((GoB f) * (1,j1)) + |[(- 1),1]|))
meets Int (cell ((GoB f),(i1 -' 1),j0))
by A24, A27, A30, A305, A310, GOBOARD6:85;
LSeg (
(((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),
(((GoB f) * (1,j1)) + |[(- 1),1]|))
misses L~ f
by A308, A311, GOBOARD8:33;
then
LSeg (
(((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),
(((GoB f) * (1,j1)) + |[(- 1),1]|))
c= (L~ f) `
by SUBSET_1:23;
then A313:
LSeg (
(((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),
(((GoB f) * (1,j1)) + |[(- 1),1]|))
c= LeftComp f
by A3, A5, A6, A55, A309, A312, Th4, NAT_1:13;
i1 -' 1
<= i1
by NAT_D:35;
then A314:
i1 -' 1
<= len (GoB f)
by A21, XXREAL_0:2;
A315:
Int (cell ((GoB f),(i1 -' 1),j1)) is
convex
by A27, A314, Th16;
Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f
by A27, A314, GOBOARD7:12;
then
Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) `
by SUBSET_1:23;
then A316:
Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f
by A30, A55, A305, A313, A308, A310, Th4, A315, GOBOARD6:89;
A317:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i1,
j1)
by A4, A5, A13, A14, A16, A17, A31, A305, A306, GOBOARD5:28;
A318:
LSeg (
(((GoB f) * (1,j1)) + |[(- 1),1]|),
(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|))
meets Int (cell ((GoB f),(i1 -' 1),j1))
by A30, A305, A308, A310, GOBOARD6:89;
LSeg (
(((GoB f) * (1,j1)) + |[(- 1),1]|),
(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|))
misses L~ f
by A308, GOBOARD8:29;
then
LSeg (
(((GoB f) * (1,j1)) + |[(- 1),1]|),
(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|))
c= (L~ f) `
by SUBSET_1:23;
then A319:
LSeg (
(((GoB f) * (1,j1)) + |[(- 1),1]|),
(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|))
c= LeftComp f
by A55, A316, A318, Th4;
A320:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A317, A319, A23, A30, A305, A306, A307, A308, Th4, A320, GOBOARD6:83;
verum end; suppose that A321:
j0 + 1
= j1
and A322:
i1 + 1
= i2
and A323:
i0 <> 1
and A324:
j1 = width (GoB f)
;
Int (left_cell (f,(k + 1))) c= LeftComp fA325:
left_cell (
f,
k)
= cell (
(GoB f),
(i1 -' 1),
j0)
by A6, A7, A10, A11, A13, A14, A30, A45, A321, GOBOARD5:27;
1
< i0
by A18, A323, XXREAL_0:1;
then A326:
1
<= i0 -' 1
by A30, A45, A321, NAT_1:13;
A327:
j1 -' 1
= j0
by A321, NAT_D:34;
A328:
(i1 -' 1) + (1 + 1) = i2
by A45, A322;
A329:
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),
(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|))
meets Int (cell ((GoB f),(i1 -' 1),j0))
by A21, A24, A27, A30, A45, A321, A326, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),
(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|))
misses L~ f
by A5, A6, A11, A14, A17, A23, A30, A31, A45, A50, A321, A324, A326, A327, A328, GOBOARD8:9;
then
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),
(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|))
c= (L~ f) `
by SUBSET_1:23;
then A330:
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),
(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|))
c= LeftComp f
by A3, A5, A6, A55, A325, A329, Th4, NAT_1:13;
i1 -' 1
<= i1
by NAT_D:35;
then A331:
i1 -' 1
<= len (GoB f)
by A21, XXREAL_0:2;
A332:
Int (cell ((GoB f),(i1 -' 1),j1)) is
convex
by A27, A331, Th16;
Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f
by A27, A331, GOBOARD7:12;
then
Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) `
by SUBSET_1:23;
then A333:
Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f
by A30, A55, A321, A330, A19, A45, A324, A326, Th4, A332, GOBOARD6:83;
A334:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i1,
j1)
by A4, A5, A13, A14, A16, A17, A31, A321, A322, GOBOARD5:28;
A335:
LSeg (
(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|))
meets Int (cell ((GoB f),(i1 -' 1),j1))
by A21, A30, A45, A321, A324, A326, GOBOARD6:83;
LSeg (
(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|))
misses L~ f
by A23, A30, A45, A321, A324, A326, A328, GOBOARD8:28;
then
LSeg (
(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|))
c= (L~ f) `
by SUBSET_1:23;
then A336:
LSeg (
(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),
(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|))
c= LeftComp f
by A55, A333, A335, Th4;
A337:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A334, A336, A20, A23, A322, A324, Th4, A337, GOBOARD6:83;
verum end; suppose that A338:
j0 + 1
= j1
and A339:
i1 + 1
= i2
and A340:
i0 = 1
and A341:
j1 <> width (GoB f)
;
Int (left_cell (f,(k + 1))) c= LeftComp fA342:
left_cell (
f,
k)
= cell (
(GoB f),
(i1 -' 1),
j0)
by A6, A7, A10, A11, A13, A14, A30, A45, A338, GOBOARD5:27;
width (GoB f) > j1
by A27, A341, XXREAL_0:1;
then A343:
width (GoB f) >= j1 + 1
by NAT_1:13;
A344:
i0 -' 1
= 0
by A340, XREAL_1:232;
A345:
LSeg (
(((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),
(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|))
meets Int (cell ((GoB f),(i1 -' 1),j0))
by A24, A27, A30, A338, A340, A344, GOBOARD6:85;
LSeg (
(((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),
(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|))
misses L~ f
by A24, A53, A338, A340, A343, GOBOARD8:31;
then
LSeg (
(((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),
(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|))
c= (L~ f) `
by SUBSET_1:23;
then A346:
LSeg (
(((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),
(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|))
c= LeftComp f
by A3, A5, A6, A55, A342, A345, Th4, NAT_1:13;
i1 -' 1
<= i1
by NAT_D:35;
then A347:
i1 -' 1
<= len (GoB f)
by A21, XXREAL_0:2;
A348:
Int (cell ((GoB f),(i1 -' 1),j1)) is
convex
by A27, A347, Th16;
Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f
by A27, A347, GOBOARD7:12;
then
Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) `
by SUBSET_1:23;
then A349:
Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f
by A30, A55, A338, A346, A26, A340, A343, A344, Th4, A348, GOBOARD6:85;
A350:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i1,
j1)
by A4, A5, A13, A14, A16, A17, A31, A338, A339, GOBOARD5:28;
A351:
LSeg (
(((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),
((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2))))))
meets Int (cell ((GoB f),(i1 -' 1),j1))
by A26, A30, A338, A340, A343, A344, GOBOARD6:85;
LSeg (
(((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),
((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2))))))
misses L~ f
by A5, A6, A11, A14, A17, A24, A30, A31, A50, A338, A339, A340, A343, GOBOARD8:18;
then
LSeg (
(((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),
((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2))))))
c= (L~ f) `
by SUBSET_1:23;
then A352:
LSeg (
(((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),
((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2))))))
c= LeftComp f
by A55, A349, A351, Th4;
A353:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A350, A352, A20, A23, A26, A338, A339, A343, Th4, A353, GOBOARD6:82;
verum end; suppose that A354:
j0 + 1
= j1
and A355:
i1 + 1
= i2
and A356:
i0 <> 1
and A357:
j1 <> width (GoB f)
;
Int (left_cell (f,(k + 1))) c= LeftComp fA358:
left_cell (
f,
k)
= cell (
(GoB f),
(i1 -' 1),
j0)
by A6, A7, A10, A11, A13, A14, A30, A45, A354, GOBOARD5:27;
1
< i0
by A18, A356, XXREAL_0:1;
then A359:
1
<= i0 -' 1
by A30, A45, A354, NAT_1:13;
width (GoB f) > j1
by A27, A357, XXREAL_0:1;
then A360:
width (GoB f) >= j1 + 1
by NAT_1:13;
A361:
(i1 -' 1) + (1 + 1) = i2
by A45, A355;
A362:
LSeg (
((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),
((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1))))))
meets Int (cell ((GoB f),(i1 -' 1),j0))
by A21, A24, A27, A30, A45, A354, A359, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),
((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1))))))
misses L~ f
by A5, A6, A11, A14, A17, A23, A24, A30, A31, A45, A50, A53, A354, A359, A360, A361, GOBOARD8:3;
then
LSeg (
((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),
((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1))))))
c= (L~ f) `
by SUBSET_1:23;
then A363:
LSeg (
((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),
((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1))))))
c= LeftComp f
by A3, A5, A6, A55, A358, A362, Th4, NAT_1:13;
i1 -' 1
<= i1
by NAT_D:35;
then A364:
i1 -' 1
<= len (GoB f)
by A21, XXREAL_0:2;
A365:
Int (cell ((GoB f),(i1 -' 1),j1)) is
convex
by A27, A364, Th16;
Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f
by A27, A364, GOBOARD7:12;
then
Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) `
by SUBSET_1:23;
then A366:
Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f
by A30, A55, A354, A363, A19, A26, A45, A359, A360, Th4, A365, GOBOARD6:82;
A367:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
i1,
j1)
by A4, A5, A13, A14, A16, A17, A31, A354, A355, GOBOARD5:28;
A368:
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),
((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1))))))
meets Int (cell ((GoB f),(i1 -' 1),j1))
by A21, A26, A30, A45, A354, A359, A360, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),
((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1))))))
misses L~ f
by A5, A6, A11, A14, A17, A23, A24, A30, A31, A45, A50, A53, A354, A359, A360, A361, GOBOARD8:15;
then
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),
((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1))))))
c= (L~ f) `
by SUBSET_1:23;
then A369:
LSeg (
((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),
((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1))))))
c= LeftComp f
by A55, A366, A368, Th4;
A370:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A367, A369, A20, A23, A26, A355, A360, Th4, A370, GOBOARD6:82;
verum end; suppose that A371:
j0 + 1
= j1
and A372:
j1 + 1
= j2
and A373:
i0 = 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA374:
left_cell (
f,
k)
= cell (
(GoB f),
0,
j0)
by A6, A7, A10, A11, A13, A14, A30, A56, A371, A373, GOBOARD5:27;
A375:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
0,
j1)
by A4, A5, A13, A14, A16, A17, A30, A31, A56, A371, A372, A373, GOBOARD5:27;
A376:
LSeg (
(((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),
(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|))
meets Int (cell ((GoB f),0,j0))
by A24, A27, A371, GOBOARD6:85;
LSeg (
(((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),
(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|))
misses L~ f
by A24, A29, A53, A371, A372, GOBOARD8:31;
then
LSeg (
(((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),
(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|))
c= (L~ f) `
by SUBSET_1:23;
then A377:
LSeg (
(((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),
(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|))
c= LeftComp f
by A3, A5, A6, A55, A374, A376, Th4, NAT_1:13;
A378:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A55, A375, A377, A26, A29, A372, Th4, A378, GOBOARD6:85;
verum end; suppose that A379:
j0 + 1
= j1
and A380:
j1 + 1
= j2
and A381:
i0 <> 1
;
Int (left_cell (f,(k + 1))) c= LeftComp fA382:
left_cell (
f,
k)
= cell (
(GoB f),
(i1 -' 1),
j0)
by A6, A7, A10, A11, A13, A14, A30, A45, A379, GOBOARD5:27;
1
< i0
by A18, A381, XXREAL_0:1;
then A383:
1
<= i0 -' 1
by A30, A45, A379, NAT_1:13;
A384:
left_cell (
f,
(k + 1))
= cell (
(GoB f),
(i1 -' 1),
j1)
by A4, A5, A13, A14, A16, A17, A31, A45, A380, GOBOARD5:27;
A385:
LSeg (
((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),
((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2)))))
meets Int (cell ((GoB f),(i1 -' 1),j0))
by A21, A24, A27, A30, A45, A379, A383, GOBOARD6:82;
LSeg (
((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),
((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2)))))
misses L~ f
by A5, A6, A11, A14, A17, A19, A24, A29, A30, A31, A45, A50, A53, A379, A380, A383, GOBOARD8:1;
then
LSeg (
((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),
((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2)))))
c= (L~ f) `
by SUBSET_1:23;
then A386:
LSeg (
((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),
((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2)))))
c= LeftComp f
by A3, A5, A6, A55, A382, A385, Th4, NAT_1:13;
A387:
Int (left_cell (f,(k + 1))) is
convex
by A4, A5, Th17;
Int (left_cell (f,(k + 1))) misses L~ f
by A4, A5, GOBOARD8:37;
then
Int (left_cell (f,(k + 1))) c= (L~ f) `
by SUBSET_1:23;
hence
Int (left_cell (f,(k + 1))) c= LeftComp f
by A30, A55, A379, A384, A386, A19, A26, A29, A45, A380, A383, Th4, A387, GOBOARD6:82;
verum end; end; end; hence
Int (left_cell (f,(k + 1))) c= LeftComp f
;
verum end; end;
end; end;
thus
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A2); verum