begin
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
i,
j being
Element of
NAT st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 2
<= width (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
(j + 1) & ( (
f /. k = (GoB f) * (i + 1),
j &
f /. (k + 2) = (GoB f) * (i + 1),
(j + 2) ) or (
f /. (k + 2) = (GoB f) * (i + 1),
j &
f /. k = (GoB f) * (i + 1),
(j + 2) ) ) holds
LSeg ((1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),(j + 1)))),
((1 / 2) * (((GoB f) * i,(j + 1)) + ((GoB f) * (i + 1),(j + 2)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
i,
j being
Element of
NAT st 1
<= i &
i + 2
<= len (GoB f) & 1
<= j &
j + 2
<= width (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
(j + 1) & ( (
f /. k = (GoB f) * (i + 2),
(j + 1) &
f /. (k + 2) = (GoB f) * (i + 1),
(j + 2) ) or (
f /. (k + 2) = (GoB f) * (i + 2),
(j + 1) &
f /. k = (GoB f) * (i + 1),
(j + 2) ) ) holds
LSeg ((1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),(j + 1)))),
((1 / 2) * (((GoB f) * i,(j + 1)) + ((GoB f) * (i + 1),(j + 2)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
i,
j being
Element of
NAT st 1
<= i &
i + 2
<= len (GoB f) & 1
<= j &
j + 2
<= width (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
(j + 1) & ( (
f /. k = (GoB f) * (i + 2),
(j + 1) &
f /. (k + 2) = (GoB f) * (i + 1),
j ) or (
f /. (k + 2) = (GoB f) * (i + 2),
(j + 1) &
f /. k = (GoB f) * (i + 1),
j ) ) holds
LSeg ((1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),(j + 1)))),
((1 / 2) * (((GoB f) * i,(j + 1)) + ((GoB f) * (i + 1),(j + 2)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
i,
j being
Element of
NAT st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 2
<= width (GoB f) &
f /. (k + 1) = (GoB f) * i,
(j + 1) & ( (
f /. k = (GoB f) * i,
j &
f /. (k + 2) = (GoB f) * i,
(j + 2) ) or (
f /. (k + 2) = (GoB f) * i,
j &
f /. k = (GoB f) * i,
(j + 2) ) ) holds
LSeg ((1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),(j + 1)))),
((1 / 2) * (((GoB f) * i,(j + 1)) + ((GoB f) * (i + 1),(j + 2)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
i,
j being
Element of
NAT st 1
<= i &
i + 2
<= len (GoB f) & 1
<= j &
j + 2
<= width (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
(j + 1) & ( (
f /. k = (GoB f) * i,
(j + 1) &
f /. (k + 2) = (GoB f) * (i + 1),
(j + 2) ) or (
f /. (k + 2) = (GoB f) * i,
(j + 1) &
f /. k = (GoB f) * (i + 1),
(j + 2) ) ) holds
LSeg ((1 / 2) * (((GoB f) * (i + 1),j) + ((GoB f) * (i + 2),(j + 1)))),
((1 / 2) * (((GoB f) * (i + 1),(j + 1)) + ((GoB f) * (i + 2),(j + 2)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
i,
j being
Element of
NAT st 1
<= i &
i + 2
<= len (GoB f) & 1
<= j &
j + 2
<= width (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
(j + 1) & ( (
f /. k = (GoB f) * i,
(j + 1) &
f /. (k + 2) = (GoB f) * (i + 1),
j ) or (
f /. (k + 2) = (GoB f) * i,
(j + 1) &
f /. k = (GoB f) * (i + 1),
j ) ) holds
LSeg ((1 / 2) * (((GoB f) * (i + 1),j) + ((GoB f) * (i + 2),(j + 1)))),
((1 / 2) * (((GoB f) * (i + 1),(j + 1)) + ((GoB f) * (i + 2),(j + 2)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
i being
Element of
NAT st 1
<= i &
i + 2
<= len (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),1 & ( (
f /. k = (GoB f) * (i + 2),1 &
f /. (k + 2) = (GoB f) * (i + 1),2 ) or (
f /. (k + 2) = (GoB f) * (i + 2),1 &
f /. k = (GoB f) * (i + 1),2 ) ) holds
LSeg (((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),1))) - |[0 ,1]|),
((1 / 2) * (((GoB f) * i,1) + ((GoB f) * (i + 1),2))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
i being
Element of
NAT st 1
<= i &
i + 2
<= len (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),1 & ( (
f /. k = (GoB f) * i,1 &
f /. (k + 2) = (GoB f) * (i + 1),2 ) or (
f /. (k + 2) = (GoB f) * i,1 &
f /. k = (GoB f) * (i + 1),2 ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),1))) - |[0 ,1]|),
((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),2))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
i being
Element of
NAT st 1
<= i &
i + 2
<= len (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
(width (GoB f)) & ( (
f /. k = (GoB f) * (i + 2),
(width (GoB f)) &
f /. (k + 2) = (GoB f) * (i + 1),
((width (GoB f)) -' 1) ) or (
f /. (k + 2) = (GoB f) * (i + 2),
(width (GoB f)) &
f /. k = (GoB f) * (i + 1),
((width (GoB f)) -' 1) ) ) holds
LSeg ((1 / 2) * (((GoB f) * i,((width (GoB f)) -' 1)) + ((GoB f) * (i + 1),(width (GoB f))))),
(((1 / 2) * (((GoB f) * i,(width (GoB f))) + ((GoB f) * (i + 1),(width (GoB f))))) + |[0 ,1]|) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
i being
Element of
NAT st 1
<= i &
i + 2
<= len (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
(width (GoB f)) & ( (
f /. k = (GoB f) * i,
(width (GoB f)) &
f /. (k + 2) = (GoB f) * (i + 1),
((width (GoB f)) -' 1) ) or (
f /. (k + 2) = (GoB f) * i,
(width (GoB f)) &
f /. k = (GoB f) * (i + 1),
((width (GoB f)) -' 1) ) ) holds
LSeg ((1 / 2) * (((GoB f) * (i + 1),((width (GoB f)) -' 1)) + ((GoB f) * (i + 2),(width (GoB f))))),
(((1 / 2) * (((GoB f) * (i + 1),(width (GoB f))) + ((GoB f) * (i + 2),(width (GoB f))))) + |[0 ,1]|) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
i,
j being
Element of
NAT st 1
<= j &
j + 1
<= width (GoB f) & 1
<= i &
i + 2
<= len (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
(j + 1) & ( (
f /. k = (GoB f) * i,
(j + 1) &
f /. (k + 2) = (GoB f) * (i + 2),
(j + 1) ) or (
f /. (k + 2) = (GoB f) * i,
(j + 1) &
f /. k = (GoB f) * (i + 2),
(j + 1) ) ) holds
LSeg ((1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),(j + 1)))),
((1 / 2) * (((GoB f) * (i + 1),j) + ((GoB f) * (i + 2),(j + 1)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
j,
i being
Element of
NAT st 1
<= j &
j + 2
<= width (GoB f) & 1
<= i &
i + 2
<= len (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
(j + 1) & ( (
f /. k = (GoB f) * (i + 1),
(j + 2) &
f /. (k + 2) = (GoB f) * (i + 2),
(j + 1) ) or (
f /. (k + 2) = (GoB f) * (i + 1),
(j + 2) &
f /. k = (GoB f) * (i + 2),
(j + 1) ) ) holds
LSeg ((1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),(j + 1)))),
((1 / 2) * (((GoB f) * (i + 1),j) + ((GoB f) * (i + 2),(j + 1)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
j,
i being
Element of
NAT st 1
<= j &
j + 2
<= width (GoB f) & 1
<= i &
i + 2
<= len (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
(j + 1) & ( (
f /. k = (GoB f) * (i + 1),
(j + 2) &
f /. (k + 2) = (GoB f) * i,
(j + 1) ) or (
f /. (k + 2) = (GoB f) * (i + 1),
(j + 2) &
f /. k = (GoB f) * i,
(j + 1) ) ) holds
LSeg ((1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),(j + 1)))),
((1 / 2) * (((GoB f) * (i + 1),j) + ((GoB f) * (i + 2),(j + 1)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
j,
i being
Element of
NAT st 1
<= j &
j + 1
<= width (GoB f) & 1
<= i &
i + 2
<= len (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
j & ( (
f /. k = (GoB f) * i,
j &
f /. (k + 2) = (GoB f) * (i + 2),
j ) or (
f /. (k + 2) = (GoB f) * i,
j &
f /. k = (GoB f) * (i + 2),
j ) ) holds
LSeg ((1 / 2) * (((GoB f) * i,j) + ((GoB f) * (i + 1),(j + 1)))),
((1 / 2) * (((GoB f) * (i + 1),j) + ((GoB f) * (i + 2),(j + 1)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
j,
i being
Element of
NAT st 1
<= j &
j + 2
<= width (GoB f) & 1
<= i &
i + 2
<= len (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
(j + 1) & ( (
f /. k = (GoB f) * (i + 1),
j &
f /. (k + 2) = (GoB f) * (i + 2),
(j + 1) ) or (
f /. (k + 2) = (GoB f) * (i + 1),
j &
f /. k = (GoB f) * (i + 2),
(j + 1) ) ) holds
LSeg ((1 / 2) * (((GoB f) * i,(j + 1)) + ((GoB f) * (i + 1),(j + 2)))),
((1 / 2) * (((GoB f) * (i + 1),(j + 1)) + ((GoB f) * (i + 2),(j + 2)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
j,
i being
Element of
NAT st 1
<= j &
j + 2
<= width (GoB f) & 1
<= i &
i + 2
<= len (GoB f) &
f /. (k + 1) = (GoB f) * (i + 1),
(j + 1) & ( (
f /. k = (GoB f) * (i + 1),
j &
f /. (k + 2) = (GoB f) * i,
(j + 1) ) or (
f /. (k + 2) = (GoB f) * (i + 1),
j &
f /. k = (GoB f) * i,
(j + 1) ) ) holds
LSeg ((1 / 2) * (((GoB f) * i,(j + 1)) + ((GoB f) * (i + 1),(j + 2)))),
((1 / 2) * (((GoB f) * (i + 1),(j + 1)) + ((GoB f) * (i + 2),(j + 2)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
j being
Element of
NAT st 1
<= j &
j + 2
<= width (GoB f) &
f /. (k + 1) = (GoB f) * 1,
(j + 1) & ( (
f /. k = (GoB f) * 1,
(j + 2) &
f /. (k + 2) = (GoB f) * 2,
(j + 1) ) or (
f /. (k + 2) = (GoB f) * 1,
(j + 2) &
f /. k = (GoB f) * 2,
(j + 1) ) ) holds
LSeg (((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 1,(j + 1)))) - |[1,0 ]|),
((1 / 2) * (((GoB f) * 1,j) + ((GoB f) * 2,(j + 1)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
j being
Element of
NAT st 1
<= j &
j + 2
<= width (GoB f) &
f /. (k + 1) = (GoB f) * 1,
(j + 1) & ( (
f /. k = (GoB f) * 1,
j &
f /. (k + 2) = (GoB f) * 2,
(j + 1) ) or (
f /. (k + 2) = (GoB f) * 1,
j &
f /. k = (GoB f) * 2,
(j + 1) ) ) holds
LSeg (((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 1,(j + 2)))) - |[1,0 ]|),
((1 / 2) * (((GoB f) * 1,(j + 1)) + ((GoB f) * 2,(j + 2)))) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
j being
Element of
NAT st 1
<= j &
j + 2
<= width (GoB f) &
f /. (k + 1) = (GoB f) * (len (GoB f)),
(j + 1) & ( (
f /. k = (GoB f) * (len (GoB f)),
(j + 2) &
f /. (k + 2) = (GoB f) * ((len (GoB f)) -' 1),
(j + 1) ) or (
f /. (k + 2) = (GoB f) * (len (GoB f)),
(j + 2) &
f /. k = (GoB f) * ((len (GoB f)) -' 1),
(j + 1) ) ) holds
LSeg ((1 / 2) * (((GoB f) * ((len (GoB f)) -' 1),j) + ((GoB f) * (len (GoB f)),(j + 1)))),
(((1 / 2) * (((GoB f) * (len (GoB f)),j) + ((GoB f) * (len (GoB f)),(j + 1)))) + |[1,0 ]|) misses L~ f
theorem
for
f being non
constant standard special_circular_sequence for
k being
Element of
NAT st 1
<= k &
k + 2
<= len f holds
for
j being
Element of
NAT st 1
<= j &
j + 2
<= width (GoB f) &
f /. (k + 1) = (GoB f) * (len (GoB f)),
(j + 1) & ( (
f /. k = (GoB f) * (len (GoB f)),
j &
f /. (k + 2) = (GoB f) * ((len (GoB f)) -' 1),
(j + 1) ) or (
f /. (k + 2) = (GoB f) * (len (GoB f)),
j &
f /. k = (GoB f) * ((len (GoB f)) -' 1),
(j + 1) ) ) holds
LSeg ((1 / 2) * (((GoB f) * ((len (GoB f)) -' 1),(j + 1)) + ((GoB f) * (len (GoB f)),(j + 2)))),
(((1 / 2) * (((GoB f) * (len (GoB f)),(j + 1)) + ((GoB f) * (len (GoB f)),(j + 2)))) + |[1,0 ]|) misses L~ f
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem