environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, FUNCT_1, GOBOARD5, XXREAL_0, ARYTM_3, FINSEQ_1, GOBOARD2, TREES_1, PARTFUN1, RELAT_1, RLTOPSP1, XBOOLE_0, TOPREAL1, TARSKI, TOPS_1, ARYTM_1, CARD_1, MCART_1, GOBOARD1, MATRIX_1, NAT_1, COMPLEX1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, NAT_1, NAT_D, PARTFUN1, FINSEQ_1, MATRIX_0, SEQM_3, STRUCT_0, PRE_TOPC, TOPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5, XXREAL_0;
definitions ;
theorems GOBOARD5, EUCLID, GOBOARD1, TOPREAL3, TOPREAL1, GOBOARD2, FINSEQ_3, NAT_1, GOBOARD6, GOBOARD7, SPPOL_2, XBOOLE_0, XBOOLE_1, ZFMISC_1, XREAL_1, XXREAL_0, XREAL_0, MATRIX_0, SEQM_3;
schemes ;
registrations RELSET_1, XREAL_0, STRUCT_0, EUCLID, GOBOARD2, GOBOARD5, ORDINAL1, NAT_1;
constructors HIDDEN, REAL_1, NAT_D, TOPS_1, GOBOARD2, GOBOARD5, GOBOARD1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
equalities ;
expansions ;
theorem
for
f being non
constant standard special_circular_sequence for
k being
Nat st 1
<= k &
k + 2
<= len f holds
for
i,
j being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
i,
j being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
i,
j being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
i,
j being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
i,
j being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
i,
j being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
i being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
i being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
i being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
i being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
i,
j being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
j,
i being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
j,
i being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
j,
i being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
j,
i being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
j,
i being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
j being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
j being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
j being
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
Nat st 1
<= k &
k + 2
<= len f holds
for
j being
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