:: GOBOARD2 semantic presentation

scheme :: GOBOARD2:sch 1
s1{ F₁() -> non empty set , F₂() -> Nat, F₃( set ) -> Element of F₁() } :

ex b₁ being FinSequence of F₁() st
( len b₁ = F₂() & ( for b₂ being Nat st b₂ in dom b₁ holds
b₁ /. b₂ = F₃(b₂) ) )

proof end;

defpred S₁[ Nat] means for b₁ being finite Subset of REAL st b₁ <> {} & card b₁ = a₁ holds
( b₁ is bounded_above & upper_bound b₁ in b₁ & b₁ is bounded_below & lower_bound b₁ in b₁ );

Lemma1: S₁[0]
by CARD_2:59;

Lemma2: for b₁ being Nat st S₁[b₁] holds
S₁[b₁ + 1]

proof end;

Lemma3: for b₁ being Nat holds S₁[b₁]
from NAT_1:sch 1(Lemma1, Lemma2);

theorem Th1: :: GOBOARD2:1

for b₁ being finite Subset of REAL st b₁ <> {} holds
( b₁ is bounded_above & upper_bound b₁ in b₁ & b₁ is bounded_below & lower_bound b₁ in b₁ )

proof end;

theorem Th2: :: GOBOARD2:2

canceled;

theorem Th3: :: GOBOARD2:3

for b₁ being Nat
for b₂ being FinSequence holds
( 1 <= b₁ & b₁ + 1 <= len b₂ iff ( b₁ in dom b₂ & b₁ + 1 in dom b₂ ) )

proof end;

theorem Th4: :: GOBOARD2:4

for b₁ being Nat
for b₂ being FinSequence holds
( 1 <= b₁ & b₁ + 2 <= len b₂ iff ( b₁ in dom b₂ & b₁ + 1 in dom b₂ & b₁ + 2 in dom b₂ ) )

proof end;

theorem Th5: :: GOBOARD2:5

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁
for b₄ being Nat st 1 <= b₄ & b₄ <= len b₃ holds
(b₂ ^ b₃) /. (b₄ + (len b₂)) = b₃ /. b₄

proof end;

theorem Th6: :: GOBOARD2:6

for b₁ being FinSequence of (TOP-REAL 2) st ( for b₂, b₃ being Nat st b₃ > b₂ + 1 & b₂ in dom b₁ & b₂ + 1 in dom b₁ & b₃ in dom b₁ & b₃ + 1 in dom b₁ holds
LSeg b₁,b₂ misses LSeg b₁,b₃ ) holds
b₁ is s.n.c.

proof end;

theorem Th7: :: GOBOARD2:7

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₁ is unfolded & b₁ is s.n.c. & b₁ is one-to-one & b₁ /. (len b₁) in LSeg b₁,b₂ & b₂ in dom b₁ & b₂ + 1 in dom b₁ holds
b₂ + 1 = len b₁

proof end;

theorem Th8: :: GOBOARD2:8

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₂ <> 0 & len b₁ = b₂ + 1 holds
L~ b₁ = (L~ (b₁ | b₂)) \/ (LSeg b₁,b₂)

proof end;

theorem Th9: :: GOBOARD2:9

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st 1 < b₂ & len b₁ = b₂ + 1 & b₁ is unfolded & b₁ is s.n.c. holds
(L~ (b₁ | b₂)) /\ (LSeg b₁,b₂) = {(b₁ /. b₂)}

proof end;

theorem Th10: :: GOBOARD2:10

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃, b₄ being Nat st len b₁ < b₃ & b₃ + 1 <= len (b₁ ^ b₂) & b₄ + (len b₁) = b₃ holds
LSeg (b₁ ^ b₂),b₃ = LSeg b₂,b₄

proof end;

theorem Th11: :: GOBOARD2:11

for b₁, b₂ being FinSequence of (TOP-REAL 2) holds L~ b₁ c= L~ (b₁ ^ b₂)

proof end;

theorem Th12: :: GOBOARD2:12

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₁ is s.n.c. holds
b₁ | b₂ is s.n.c.

proof end;

theorem Th13: :: GOBOARD2:13

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ is special & b₂ is special & ( (b₁ /. (len b₁)) `1 = (b₂ /. 1) `1 or (b₁ /. (len b₁)) `2 = (b₂ /. 1) `2 ) holds
b₁ ^ b₂ is special

proof end;

theorem Th14: :: GOBOARD2:14

for b₁ being FinSequence of (TOP-REAL 2) st b₁ <> {} holds
X_axis b₁ <> {}

proof end;

theorem Th15: :: GOBOARD2:15

for b₁ being FinSequence of (TOP-REAL 2) st b₁ <> {} holds
Y_axis b₁ <> {}

proof end;

registration

let c₁ be non empty FinSequence of (TOP-REAL 2);
cluster X_axis a₁ -> non empty ;
coherence by Th14;
cluster Y_axis a₁ -> non empty ;
coherence by Th15;

end;

theorem Th16: :: GOBOARD2:16

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Go-board st b₁ is special holds
for b₃ being Nat st b₃ in dom b₁ & b₃ + 1 in dom b₁ holds
for b₄, b₅, b₆, b₇ being Nat st [b₄,b₅] in Indices b₂ & [b₆,b₇] in Indices b₂ & b₁ /. b₃ = b₂ * b₄,b₅ & b₁ /. (b₃ + 1) = b₂ * b₆,b₇ & not b₄ = b₆ holds
b₇ = b₅

proof end;

theorem Th17: :: GOBOARD2:17

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Go-board st ( for b₃ being Nat st b₃ in dom b₁ holds
ex b₄, b₅ being Nat st
( [b₄,b₅] in Indices b₂ & b₁ /. b₃ = b₂ * b₄,b₅ ) ) & b₁ is special & ( for b₃ being Nat st b₃ in dom b₁ & b₃ + 1 in dom b₁ holds
b₁ /. b₃ <> b₁ /. (b₃ + 1) ) holds
ex b₃ being FinSequence of (TOP-REAL 2) st
( b₃ is_sequence_on b₂ & L~ b₁ = L~ b₃ & b₃ /. 1 = b₁ /. 1 & b₃ /. (len b₃) = b₁ /. (len b₁) & len b₁ <= len b₃ )

proof end;

theorem Th18: :: GOBOARD2:18

for b₁ being FinSequence of REAL st b₁ is increasing holds
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & b₂ <= b₃ holds
b₁ . b₂ <= b₁ . b₃

proof end;

theorem Th19: :: GOBOARD2:19

for b₁ being FinSequence of REAL st b₁ is increasing holds
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & b₂ <> b₃ holds
b₁ . b₂ <> b₁ . b₃

proof end;

theorem Th20: :: GOBOARD2:20

for b₁, b₂ being FinSequence of REAL
for b₃ being Nat st b₁ is increasing & b₂ = b₁ | (Seg b₃) holds
b₂ is increasing

proof end;

defpred S₂[ Nat] means for b₁ being FinSequence of REAL st card (rng b₁) = a₁ holds
ex b₂ being FinSequence of REAL st
( rng b₂ = rng b₁ & len b₂ = card (rng b₁) & b₂ is increasing );

Lemma15: S₂[0]

proof end;

Lemma16: for b₁ being Nat st S₂[b₁] holds
S₂[b₁ + 1]

proof end;

Lemma17: for b₁ being Nat holds S₂[b₁]
from NAT_1:sch 1(Lemma15, Lemma16);

theorem Th21: :: GOBOARD2:21

for b₁ being FinSequence of REAL ex b₂ being FinSequence of REAL st
( rng b₂ = rng b₁ & len b₂ = card (rng b₁) & b₂ is increasing ) by Lemma17;

defpred S₃[ Nat] means for b₁, b₂ being FinSequence of REAL st len b₁ = a₁ & len b₂ = a₁ & rng b₁ = rng b₂ & b₁ is increasing & b₂ is increasing holds
b₁ = b₂;

Lemma18: S₃[0]

proof end;

Lemma19: for b₁ being Nat st S₃[b₁] holds
S₃[b₁ + 1]

proof end;

Lemma20: for b₁ being Nat holds S₃[b₁]
from NAT_1:sch 1(Lemma18, Lemma19);

theorem Th22: :: GOBOARD2:22

for b₁, b₂ being FinSequence of REAL st len b₁ = len b₂ & rng b₁ = rng b₂ & b₁ is increasing & b₂ is increasing holds
b₁ = b₂ by Lemma20;

definition

let c₁, c₂ be increasing FinSequence of REAL ;
assume E21: ( c₁ <> {} & c₂ <> {} ) ;
func GoB c₁,c₂ -> Matrix of (TOP-REAL 2) means :Def1: :: GOBOARD2:def 1
( len a₃ = len a₁ & width a₃ = len a₂ & ( for b₁, b₂ being Nat st [b₁,b₂] in Indices a₃ holds
a₃ * b₁,b₂ = |[(a₁ . b₁),(a₂ . b₂)]| ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines GoB GOBOARD2:def 1 :

registration

let c₁, c₂ be non empty increasing FinSequence of REAL ;
cluster GoB a₁,a₂ -> V4 X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ;
coherence

proof end;

end;

definition

let c₁ be FinSequence of REAL ;
func Incr c₁ -> increasing FinSequence of REAL means :Def2: :: GOBOARD2:def 2
( rng a₂ = rng a₁ & len a₂ = card (rng a₁) );
existence

proof end;

uniqueness by Lemma20;

end;

:: deftheorem Def2 defines Incr GOBOARD2:def 2 :

definition

let c₁ be non empty FinSequence of (TOP-REAL 2);
func GoB c₁ -> Matrix of (TOP-REAL 2) equals :: GOBOARD2:def 3
GoB (Incr (X_axis a₁)),(Incr (Y_axis a₁));
correctness ;

end;

:: deftheorem Def3 defines GoB GOBOARD2:def 3 :

theorem Th23: :: GOBOARD2:23

for b₁ being FinSequence of REAL st b₁ <> {} holds
Incr b₁ <> {}

proof end;

registration

let c₁ be non empty FinSequence of REAL ;
cluster Incr a₁ -> non empty increasing ;
coherence by Th23;

end;

registration

let c₁ be non empty FinSequence of (TOP-REAL 2);
cluster GoB a₁ -> V4 X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ;
coherence ;

end;

theorem Th24: :: GOBOARD2:24

for b₁ being non empty FinSequence of (TOP-REAL 2) holds
( len (GoB b₁) = card (rng (X_axis b₁)) & width (GoB b₁) = card (rng (Y_axis b₁)) )

proof end;

theorem Th25: :: GOBOARD2:25

for b₁ being non empty FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₂ in dom b₁ holds
ex b₃, b₄ being Nat st
( [b₃,b₄] in Indices (GoB b₁) & b₁ /. b₂ = (GoB b₁) * b₃,b₄ )

proof end;

theorem Th26: :: GOBOARD2:26

for b₁ being Nat
for b₂ being non empty FinSequence of (TOP-REAL 2) st b₁ in dom b₂ & ( for b₃ being Nat st b₃ in dom b₂ holds
(X_axis b₂) . b₁ <= (X_axis b₂) . b₃ ) holds
b₂ /. b₁ in rng (Line (GoB b₂),1)

proof end;

theorem Th27: :: GOBOARD2:27

for b₁ being Nat
for b₂ being non empty FinSequence of (TOP-REAL 2) st b₁ in dom b₂ & ( for b₃ being Nat st b₃ in dom b₂ holds
(X_axis b₂) . b₃ <= (X_axis b₂) . b₁ ) holds
b₂ /. b₁ in rng (Line (GoB b₂),(len (GoB b₂)))

proof end;

theorem Th28: :: GOBOARD2:28

for b₁ being Nat
for b₂ being non empty FinSequence of (TOP-REAL 2) st b₁ in dom b₂ & ( for b₃ being Nat st b₃ in dom b₂ holds
(Y_axis b₂) . b₁ <= (Y_axis b₂) . b₃ ) holds
b₂ /. b₁ in rng (Col (GoB b₂),1)

proof end;

theorem Th29: :: GOBOARD2:29

for b₁ being Nat
for b₂ being non empty FinSequence of (TOP-REAL 2) st b₁ in dom b₂ & ( for b₃ being Nat st b₃ in dom b₂ holds
(Y_axis b₂) . b₃ <= (Y_axis b₂) . b₁ ) holds
b₂ /. b₁ in rng (Col (GoB b₂),(width (GoB b₂)))

proof end;