let f be non constant standard special_circular_sequence; :: thesis: 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 :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
thus S1[k + 1] :: thesis: verum
proof
assume that
A4: 1 <= k + 1 and
A5: (k + 1) + 1 <= len f ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
per cases ( k = 0 or k >= 1 ) by NAT_1:14;
suppose k = 0 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
hence Int (left_cell (f,(k + 1))) c= LeftComp f by Def1; :: thesis: verum
end;
suppose A6: k >= 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A7: 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 :: thesis: ( i0 = i2 implies not j0 = j2 )
assume that
A40: i0 = i2 and
A41: j0 = j2 ; :: thesis: contradiction
A42: now :: thesis: ( k <= 1 implies not (k + 1) + 1 >= len f )
assume k <= 1 ; :: thesis: not (k + 1) + 1 >= len f
then A43: k = 1 by A6, XXREAL_0:1;
assume (k + 1) + 1 >= len f ; :: thesis: contradiction
then (k + 1) + 1 = len f by A5, XXREAL_0:1;
hence contradiction by A43, GOBOARD7:34; :: thesis: verum
end;
A44: 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 :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
per 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 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A60: 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; :: thesis: verum
end;
suppose that A65: i0 = i1 + 1 and
A66: i1 = i2 + 1 and
A67: j0 <> 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A68: 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; :: thesis: verum
end;
suppose that A74: i0 = i1 + 1 and
A75: j1 = j2 + 1 ; :: thesis: 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; :: thesis: verum
end;
suppose that A76: j0 = j1 + 1 and
A77: i1 = i2 + 1 and
A78: i0 = len (GoB f) and
A79: j1 = 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A80: 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; :: thesis: verum
end;
suppose that A89: j0 = j1 + 1 and
A90: i1 = i2 + 1 and
A91: i0 <> len (GoB f) and
A92: j1 = 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A93: 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; :: thesis: verum
end;
suppose that A103: j0 = j1 + 1 and
A104: i1 = i2 + 1 and
A105: i0 = len (GoB f) and
A106: j1 <> 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A107: 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; :: thesis: verum
end;
suppose that A120: j0 = j1 + 1 and
A121: i1 = i2 + 1 and
A122: i0 <> len (GoB f) and
A123: j1 <> 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A124: 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; :: thesis: verum
end;
suppose that A137: j0 = j1 + 1 and
A138: j1 = j2 + 1 and
A139: i0 = len (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A140: 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; :: thesis: verum
end;
suppose that A145: j0 = j1 + 1 and
A146: j1 = j2 + 1 and
A147: i0 <> len (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A148: 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; :: thesis: 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) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A158: 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; :: thesis: 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) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A171: 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; :: thesis: 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) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A185: 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; :: thesis: 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) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A199: 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; :: thesis: verum
end;
suppose that A210: j0 + 1 = j1 and
A211: i1 = i2 + 1 ; :: thesis: 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; :: thesis: verum
end;
suppose that A212: i0 = i1 + 1 and
A213: j1 + 1 = j2 and
A214: i1 = 1 and
A215: j1 = 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A216: 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; :: thesis: verum
end;
suppose that A229: i0 = i1 + 1 and
A230: j1 + 1 = j2 and
A231: i1 <> 1 and
A232: j1 = 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A233: 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; :: thesis: verum
end;
suppose that A247: i0 = i1 + 1 and
A248: j1 + 1 = j2 and
A249: i1 = 1 and
A250: j1 <> 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A251: 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; :: thesis: verum
end;
suppose that A265: i0 = i1 + 1 and
A266: j1 + 1 = j2 and
A267: i1 <> 1 and
A268: j1 <> 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A269: 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; :: thesis: verum
end;
suppose that A284: j0 = j1 + 1 and
A285: i1 + 1 = i2 ; :: thesis: 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; :: thesis: verum
end;
suppose that A286: i0 + 1 = i1 and
A287: i1 + 1 = i2 and
A288: j0 = width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A289: 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; :: thesis: verum
end;
suppose that A294: i0 + 1 = i1 and
A295: i1 + 1 = i2 and
A296: j0 <> width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A297: 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; :: thesis: verum
end;
suppose that A303: i0 + 1 = i1 and
A304: j1 + 1 = j2 ; :: thesis: 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; :: thesis: verum
end;
suppose that A305: j0 + 1 = j1 and
A306: i1 + 1 = i2 and
A307: i0 = 1 and
A308: j1 = width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A309: 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; :: thesis: verum
end;
suppose that A321: j0 + 1 = j1 and
A322: i1 + 1 = i2 and
A323: i0 <> 1 and
A324: j1 = width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A325: 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; :: thesis: verum
end;
suppose that A338: j0 + 1 = j1 and
A339: i1 + 1 = i2 and
A340: i0 = 1 and
A341: j1 <> width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A342: 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; :: thesis: verum
end;
suppose that A354: j0 + 1 = j1 and
A355: i1 + 1 = i2 and
A356: i0 <> 1 and
A357: j1 <> width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A358: 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; :: thesis: verum
end;
suppose that A371: j0 + 1 = j1 and
A372: j1 + 1 = j2 and
A373: i0 = 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A374: 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; :: thesis: verum
end;
suppose that A379: j0 + 1 = j1 and
A380: j1 + 1 = j2 and
A381: i0 <> 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A382: 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; :: thesis: verum
end;
end;
end;
hence Int (left_cell (f,(k + 1))) c= LeftComp f ; :: thesis: verum
end;
end;
end;
end;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A1, A2); :: thesis: verum