environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FINSEQ_1, EUCLID, REAL_1, PRE_TOPC, GOBOARD1, COMPLEX1, ARYTM_1, XXREAL_0, ARYTM_3, CARD_1, SUPINF_2, RLTOPSP1, MCART_1, RELAT_1, TREES_1, SPPOL_1, GOBOARD2, MATRIX_1, PARTFUN1, TOPREAL1, TOPS_1, GOBOARD5, TARSKI, FUNCT_1, FINSET_1, FINSEQ_6, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0, XCMPLX_0, COMPLEX1, REAL_1, XREAL_0, NAT_1, INT_2, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSET_1, STRUCT_0, MATRIX_0, MATRIX_1, PRE_TOPC, TOPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, SPPOL_1, FINSEQ_6, GOBOARD5;
definitions TARSKI;
theorems GOBOARD5, TOPS_1, EUCLID, GOBOARD1, TOPREAL3, ABSVALUE, TARSKI, SPPOL_1, TOPREAL1, GOBOARD2, FINSEQ_3, NAT_1, FINSEQ_6, GOBOARD6, MATRIX_0, FINSEQ_1, CARD_2, FINSEQ_5, XBOOLE_0, XREAL_1, FUNCT_1, XXREAL_0, RLTOPSP1, SEQM_3, RLVECT_1;
schemes NAT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, INT_1, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2, GOBOARD5, FINSET_1, CARD_1, XREAL_0, NAT_1;
constructors HIDDEN, PARTFUN1, XXREAL_0, REAL_1, NAT_1, INT_2, NAT_D, TOPS_1, GOBOARD2, SPPOL_1, GOBOARD5, GOBOARD1, DOMAIN_1, BINOP_2, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RLTOPSP1, RLVECT_1;
expansions ;
theorem Th1:
for
s,
r1,
r2 being
Real holds
( not
|.(r1 - r2).| > s or
r1 + s < r2 or
r2 + s < r1 )
theorem
for
G being
Go-board for
i1,
j1,
i2,
j2 being
Nat st 1
<= i1 &
i1 <= len G & 1
<= j1 &
j1 + 1
<= width G & 1
<= i2 &
i2 <= len G & 1
<= j2 &
j2 + 1
<= width G &
LSeg (
(G * (i1,j1)),
(G * (i1,(j1 + 1))))
meets LSeg (
(G * (i2,j2)),
(G * (i2,(j2 + 1)))) & not (
j1 = j2 &
LSeg (
(G * (i1,j1)),
(G * (i1,(j1 + 1))))
= LSeg (
(G * (i2,j2)),
(G * (i2,(j2 + 1)))) ) & not (
j1 = j2 + 1 &
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1))))) = {(G * (i1,j1))} ) holds
(
j1 + 1
= j2 &
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1))))) = {(G * (i2,j2))} )
theorem
for
G being
Go-board for
i1,
j1,
i2,
j2 being
Nat st 1
<= i1 &
i1 + 1
<= len G & 1
<= j1 &
j1 <= width G & 1
<= i2 &
i2 + 1
<= len G & 1
<= j2 &
j2 <= width G &
LSeg (
(G * (i1,j1)),
(G * ((i1 + 1),j1)))
meets LSeg (
(G * (i2,j2)),
(G * ((i2 + 1),j2))) & not (
i1 = i2 &
LSeg (
(G * (i1,j1)),
(G * ((i1 + 1),j1)))
= LSeg (
(G * (i2,j2)),
(G * ((i2 + 1),j2))) ) & not (
i1 = i2 + 1 &
(LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i1,j1))} ) holds
(
i1 + 1
= i2 &
(LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i2,j2))} )
theorem
for
G being
Go-board for
i1,
j1,
i2,
j2 being
Nat st 1
<= i1 &
i1 <= len G & 1
<= j1 &
j1 + 1
<= width G & 1
<= i2 &
i2 + 1
<= len G & 1
<= j2 &
j2 <= width G &
LSeg (
(G * (i1,j1)),
(G * (i1,(j1 + 1))))
meets LSeg (
(G * (i2,j2)),
(G * ((i2 + 1),j2))) & not (
j1 = j2 &
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i1,j1))} ) holds
(
j1 + 1
= j2 &
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i1,(j1 + 1)))} )
Lm1:
1 - (1 / 2) = 1 / 2
;
Lm2:
for f being non constant standard special_circular_sequence holds len f > 1
theorem
for
i,
j,
k being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 1
<= width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * ((i + 1),(j + 1))))
= LSeg (
f,
k) &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 1),(j + 1))))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
i,
(j + 1)) &
f /. (k + 1) = (GoB f) * (
(i + 1),
(j + 1)) &
f /. (k + 2) = (GoB f) * (
(i + 1),
j) )
theorem
for
i,
j,
k being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i <= len (GoB f) & 1
<= j &
j + 1
< width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * (i,(j + 2))))
= LSeg (
f,
k) &
LSeg (
((GoB f) * (i,j)),
((GoB f) * (i,(j + 1))))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
i,
(j + 2)) &
f /. (k + 1) = (GoB f) * (
i,
(j + 1)) &
f /. (k + 2) = (GoB f) * (
i,
j) )
theorem
for
i,
j,
k being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 1
<= width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * ((i + 1),(j + 1))))
= LSeg (
f,
k) &
LSeg (
((GoB f) * (i,j)),
((GoB f) * (i,(j + 1))))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
(i + 1),
(j + 1)) &
f /. (k + 1) = (GoB f) * (
i,
(j + 1)) &
f /. (k + 2) = (GoB f) * (
i,
j) )
theorem
for
i,
j,
k being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 1
<= width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 1),(j + 1))))
= LSeg (
f,
k) &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * ((i + 1),(j + 1))))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
(i + 1),
j) &
f /. (k + 1) = (GoB f) * (
(i + 1),
(j + 1)) &
f /. (k + 2) = (GoB f) * (
i,
(j + 1)) )
theorem
for
i,
j,
k being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
< len (GoB f) & 1
<= j &
j <= width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 2),j)))
= LSeg (
f,
k) &
LSeg (
((GoB f) * (i,j)),
((GoB f) * ((i + 1),j)))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
(i + 2),
j) &
f /. (k + 1) = (GoB f) * (
(i + 1),
j) &
f /. (k + 2) = (GoB f) * (
i,
j) )
theorem
for
i,
j,
k being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 1
<= width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 1),(j + 1))))
= LSeg (
f,
k) &
LSeg (
((GoB f) * (i,j)),
((GoB f) * ((i + 1),j)))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
(i + 1),
(j + 1)) &
f /. (k + 1) = (GoB f) * (
(i + 1),
j) &
f /. (k + 2) = (GoB f) * (
i,
j) )
theorem
for
i,
j,
k being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 1
<= width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 1),(j + 1))))
= LSeg (
f,
k) &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * ((i + 1),(j + 1))))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
(i + 1),
j) &
f /. (k + 1) = (GoB f) * (
(i + 1),
(j + 1)) &
f /. (k + 2) = (GoB f) * (
i,
(j + 1)) )
theorem
for
i,
j,
k being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i <= len (GoB f) & 1
<= j &
j + 1
< width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * (i,j)),
((GoB f) * (i,(j + 1))))
= LSeg (
f,
k) &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * (i,(j + 2))))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
i,
j) &
f /. (k + 1) = (GoB f) * (
i,
(j + 1)) &
f /. (k + 2) = (GoB f) * (
i,
(j + 2)) )
theorem
for
i,
j,
k being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 1
<= width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * (i,j)),
((GoB f) * (i,(j + 1))))
= LSeg (
f,
k) &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * ((i + 1),(j + 1))))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
i,
j) &
f /. (k + 1) = (GoB f) * (
i,
(j + 1)) &
f /. (k + 2) = (GoB f) * (
(i + 1),
(j + 1)) )
theorem
for
i,
j,
k being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 1
<= width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * ((i + 1),(j + 1))))
= LSeg (
f,
k) &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 1),(j + 1))))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
i,
(j + 1)) &
f /. (k + 1) = (GoB f) * (
(i + 1),
(j + 1)) &
f /. (k + 2) = (GoB f) * (
(i + 1),
j) )
theorem
for
i,
j,
k being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
< len (GoB f) & 1
<= j &
j <= width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * (i,j)),
((GoB f) * ((i + 1),j)))
= LSeg (
f,
k) &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 2),j)))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
i,
j) &
f /. (k + 1) = (GoB f) * (
(i + 1),
j) &
f /. (k + 2) = (GoB f) * (
(i + 2),
j) )
theorem
for
i,
j,
k being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 1
<= width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * (i,j)),
((GoB f) * ((i + 1),j)))
= LSeg (
f,
k) &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 1),(j + 1))))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
i,
j) &
f /. (k + 1) = (GoB f) * (
(i + 1),
j) &
f /. (k + 2) = (GoB f) * (
(i + 1),
(j + 1)) )
theorem Th53:
for
i,
j being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i <= len (GoB f) & 1
<= j &
j + 1
< width (GoB f) &
LSeg (
((GoB f) * (i,j)),
((GoB f) * (i,(j + 1))))
c= L~ f &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * (i,(j + 2))))
c= L~ f & not (
f /. 1
= (GoB f) * (
i,
(j + 1)) & ( (
f /. 2
= (GoB f) * (
i,
j) &
f /. ((len f) -' 1) = (GoB f) * (
i,
(j + 2)) ) or (
f /. 2
= (GoB f) * (
i,
(j + 2)) &
f /. ((len f) -' 1) = (GoB f) * (
i,
j) ) ) ) holds
ex
k being
Nat st
( 1
<= k &
k + 1
< len 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 = (GoB f) * (
i,
(j + 2)) &
f /. (k + 2) = (GoB f) * (
i,
j) ) ) )
theorem Th54:
for
i,
j being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 1
<= width (GoB f) &
LSeg (
((GoB f) * (i,j)),
((GoB f) * (i,(j + 1))))
c= L~ f &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * ((i + 1),(j + 1))))
c= L~ f & not (
f /. 1
= (GoB f) * (
i,
(j + 1)) & ( (
f /. 2
= (GoB f) * (
i,
j) &
f /. ((len f) -' 1) = (GoB f) * (
(i + 1),
(j + 1)) ) or (
f /. 2
= (GoB f) * (
(i + 1),
(j + 1)) &
f /. ((len f) -' 1) = (GoB f) * (
i,
j) ) ) ) holds
ex
k being
Nat st
( 1
<= k &
k + 1
< len f &
f /. (k + 1) = (GoB f) * (
i,
(j + 1)) & ( (
f /. k = (GoB f) * (
i,
j) &
f /. (k + 2) = (GoB f) * (
(i + 1),
(j + 1)) ) or (
f /. k = (GoB f) * (
(i + 1),
(j + 1)) &
f /. (k + 2) = (GoB f) * (
i,
j) ) ) )
theorem Th55:
for
i,
j being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 1
<= width (GoB f) &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * ((i + 1),(j + 1))))
c= L~ f &
LSeg (
((GoB f) * ((i + 1),(j + 1))),
((GoB f) * ((i + 1),j)))
c= L~ f & not (
f /. 1
= (GoB f) * (
(i + 1),
(j + 1)) & ( (
f /. 2
= (GoB f) * (
i,
(j + 1)) &
f /. ((len f) -' 1) = (GoB f) * (
(i + 1),
j) ) or (
f /. 2
= (GoB f) * (
(i + 1),
j) &
f /. ((len f) -' 1) = (GoB f) * (
i,
(j + 1)) ) ) ) holds
ex
k being
Nat st
( 1
<= k &
k + 1
< len 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 = (GoB f) * (
(i + 1),
j) &
f /. (k + 2) = (GoB f) * (
i,
(j + 1)) ) ) )
theorem Th56:
for
i,
j being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
< len (GoB f) & 1
<= j &
j <= width (GoB f) &
LSeg (
((GoB f) * (i,j)),
((GoB f) * ((i + 1),j)))
c= L~ f &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 2),j)))
c= L~ f & not (
f /. 1
= (GoB f) * (
(i + 1),
j) & ( (
f /. 2
= (GoB f) * (
i,
j) &
f /. ((len f) -' 1) = (GoB f) * (
(i + 2),
j) ) or (
f /. 2
= (GoB f) * (
(i + 2),
j) &
f /. ((len f) -' 1) = (GoB f) * (
i,
j) ) ) ) holds
ex
k being
Nat st
( 1
<= k &
k + 1
< len 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 = (GoB f) * (
(i + 2),
j) &
f /. (k + 2) = (GoB f) * (
i,
j) ) ) )
theorem Th57:
for
i,
j being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 1
<= width (GoB f) &
LSeg (
((GoB f) * (i,j)),
((GoB f) * ((i + 1),j)))
c= L~ f &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 1),(j + 1))))
c= L~ f & not (
f /. 1
= (GoB f) * (
(i + 1),
j) & ( (
f /. 2
= (GoB f) * (
i,
j) &
f /. ((len f) -' 1) = (GoB f) * (
(i + 1),
(j + 1)) ) or (
f /. 2
= (GoB f) * (
(i + 1),
(j + 1)) &
f /. ((len f) -' 1) = (GoB f) * (
i,
j) ) ) ) holds
ex
k being
Nat st
( 1
<= k &
k + 1
< len f &
f /. (k + 1) = (GoB f) * (
(i + 1),
j) & ( (
f /. k = (GoB f) * (
i,
j) &
f /. (k + 2) = (GoB f) * (
(i + 1),
(j + 1)) ) or (
f /. k = (GoB f) * (
(i + 1),
(j + 1)) &
f /. (k + 2) = (GoB f) * (
i,
j) ) ) )
theorem Th58:
for
i,
j being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i + 1
<= len (GoB f) & 1
<= j &
j + 1
<= width (GoB f) &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 1),(j + 1))))
c= L~ f &
LSeg (
((GoB f) * ((i + 1),(j + 1))),
((GoB f) * (i,(j + 1))))
c= L~ f & not (
f /. 1
= (GoB f) * (
(i + 1),
(j + 1)) & ( (
f /. 2
= (GoB f) * (
(i + 1),
j) &
f /. ((len f) -' 1) = (GoB f) * (
i,
(j + 1)) ) or (
f /. 2
= (GoB f) * (
i,
(j + 1)) &
f /. ((len f) -' 1) = (GoB f) * (
(i + 1),
j) ) ) ) holds
ex
k being
Nat st
( 1
<= k &
k + 1
< len 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 = (GoB f) * (
i,
(j + 1)) &
f /. (k + 2) = (GoB f) * (
(i + 1),
j) ) ) )
theorem
for
i,
j being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i < len (GoB f) & 1
<= j &
j + 1
< width (GoB f) &
LSeg (
((GoB f) * (i,j)),
((GoB f) * (i,(j + 1))))
c= L~ f &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * (i,(j + 2))))
c= L~ f holds
not
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * ((i + 1),(j + 1))))
c= L~ f
theorem
for
i,
j being
Nat for
f being non
constant standard special_circular_sequence st 1
<= i &
i < len (GoB f) & 1
<= j &
j + 1
< width (GoB f) &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 1),(j + 1))))
c= L~ f &
LSeg (
((GoB f) * ((i + 1),(j + 1))),
((GoB f) * ((i + 1),(j + 2))))
c= L~ f holds
not
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * ((i + 1),(j + 1))))
c= L~ f
theorem
for
i,
j being
Nat for
f being non
constant standard special_circular_sequence st 1
<= j &
j < width (GoB f) & 1
<= i &
i + 1
< len (GoB f) &
LSeg (
((GoB f) * (i,j)),
((GoB f) * ((i + 1),j)))
c= L~ f &
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 2),j)))
c= L~ f holds
not
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 1),(j + 1))))
c= L~ f
theorem
for
i,
j being
Nat for
f being non
constant standard special_circular_sequence st 1
<= j &
j < width (GoB f) & 1
<= i &
i + 1
< len (GoB f) &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * ((i + 1),(j + 1))))
c= L~ f &
LSeg (
((GoB f) * ((i + 1),(j + 1))),
((GoB f) * ((i + 2),(j + 1))))
c= L~ f holds
not
LSeg (
((GoB f) * ((i + 1),j)),
((GoB f) * ((i + 1),(j + 1))))
c= L~ f