:: GOBRD13 semantic presentation

definition

let c₁ be non empty set ;
let c₂ be FinSequence-DOMAIN of the carrier of (TOP-REAL 2);
let c₃ be Function of c₁,c₂;
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> FinSequence of (TOP-REAL 2);
coherence

proof end;

end;

definition

let c₁ be Function;
func Values c₁ -> set equals :: GOBRD13:def 1
Union (rngs a₁);
correctness ;

end;

:: deftheorem Def1 defines Values GOBRD13:def 1 :

theorem Th1: :: GOBRD13:1

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ * holds b₃ . b₁ is FinSequence of b₂

proof end;

registration

let c₁ be set ;
cluster -> FinSequence-yielding FinSequence of a₁ * ;
coherence

proof end;

end;

registration

cluster FinSequence-yielding -> Function-yielding set ;
coherence

proof end;

end;

theorem Th2: :: GOBRD13:2

canceled;

theorem Th3: :: GOBRD13:3

for b₁ being non empty set
for b₂ being FinSequence of b₁ * holds Values b₂ = union { (rng b₃) where B is Element of b₁ * : b₃ in rng b₂ }

proof end;

registration

let c₁ be non empty set ;
let c₂ be FinSequence of c₁ * ;
cluster Values a₂ -> finite ;
coherence

proof end;

end;

theorem Th4: :: GOBRD13:4

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂
for b₄ being Matrix of b₂ st b₁ in dom b₄ & b₄ . b₁ = b₃ holds
len b₃ = width b₄

proof end;

theorem Th5: :: GOBRD13:5

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃
for b₅ being Matrix of b₃ st b₁ in dom b₅ & b₅ . b₁ = b₄ & b₂ in dom b₄ holds
[b₁,b₂] in Indices b₅

proof end;

theorem Th6: :: GOBRD13:6

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃
for b₅ being Matrix of b₃ st [b₁,b₂] in Indices b₅ & b₅ . b₁ = b₄ holds
( len b₄ = width b₅ & b₂ in dom b₄ )

proof end;

theorem Th7: :: GOBRD13:7

for b₁ being non empty set
for b₂ being Matrix of b₁ holds Values b₂ = { (b₂ * b₃,b₄) where B is Nat, B is Nat : [b₃,b₄] in Indices b₂ }

proof end;

theorem Th8: :: GOBRD13:8

for b₁ being non empty set
for b₂ being Matrix of b₁ holds card (Values b₂) <= (len b₂) * (width b₂)

proof end;

theorem Th9: :: GOBRD13:9

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Matrix of (TOP-REAL 2) st b₁ is_sequence_on b₂ holds
rng b₁ c= Values b₂

proof end;

theorem Th10: :: GOBRD13:10

for b₁, b₂, b₃ being Nat
for b₄, b₅ being Go-board st Values b₄ c= Values b₅ & [b₁,b₂] in Indices b₄ & 1 <= b₃ & b₃ <= width b₅ & b₄ * b₁,b₂ = b₅ * 1,b₃ holds
b₁ = 1

proof end;

theorem Th11: :: GOBRD13:11

for b₁, b₂, b₃ being Nat
for b₄, b₅ being Go-board st Values b₄ c= Values b₅ & [b₁,b₂] in Indices b₄ & 1 <= b₃ & b₃ <= width b₅ & b₄ * b₁,b₂ = b₅ * (len b₅),b₃ holds
b₁ = len b₄

proof end;

theorem Th12: :: GOBRD13:12

for b₁, b₂, b₃ being Nat
for b₄, b₅ being Go-board st Values b₄ c= Values b₅ & [b₁,b₂] in Indices b₄ & 1 <= b₃ & b₃ <= len b₅ & b₄ * b₁,b₂ = b₅ * b₃,1 holds
b₂ = 1

proof end;

theorem Th13: :: GOBRD13:13

for b₁, b₂, b₃ being Nat
for b₄, b₅ being Go-board st Values b₄ c= Values b₅ & [b₁,b₂] in Indices b₄ & 1 <= b₃ & b₃ <= len b₅ & b₄ * b₁,b₂ = b₅ * b₃,(width b₅) holds
b₂ = width b₄

proof end;

theorem Th14: :: GOBRD13:14

for b₁, b₂, b₃, b₄ being Nat
for b₅, b₆ being Go-board st Values b₅ c= Values b₆ & 1 <= b₁ & b₁ < len b₅ & 1 <= b₂ & b₂ <= width b₅ & 1 <= b₃ & b₃ < len b₆ & 1 <= b₄ & b₄ <= width b₆ & b₅ * b₁,b₂ = b₆ * b₃,b₄ holds
(b₆ * (b₃ + 1),b₄) `1 <= (b₅ * (b₁ + 1),b₂) `1

proof end;

theorem Th15: :: GOBRD13:15

for b₁, b₂, b₃, b₄ being Nat
for b₅, b₆ being Go-board st b₅ * (b₁ -' 1),b₂ in Values b₆ & 1 < b₁ & b₁ <= len b₅ & 1 <= b₂ & b₂ <= width b₅ & 1 < b₃ & b₃ <= len b₆ & 1 <= b₄ & b₄ <= width b₆ & b₅ * b₁,b₂ = b₆ * b₃,b₄ holds
(b₅ * (b₁ -' 1),b₂) `1 <= (b₆ * (b₃ -' 1),b₄) `1

proof end;

theorem Th16: :: GOBRD13:16

for b₁, b₂, b₃, b₄ being Nat
for b₅, b₆ being Go-board st b₅ * b₁,(b₂ + 1) in Values b₆ & 1 <= b₁ & b₁ <= len b₅ & 1 <= b₂ & b₂ < width b₅ & 1 <= b₃ & b₃ <= len b₆ & 1 <= b₄ & b₄ < width b₆ & b₅ * b₁,b₂ = b₆ * b₃,b₄ holds
(b₆ * b₃,(b₄ + 1)) `2 <= (b₅ * b₁,(b₂ + 1)) `2

proof end;

theorem Th17: :: GOBRD13:17

for b₁, b₂, b₃, b₄ being Nat
for b₅, b₆ being Go-board st Values b₅ c= Values b₆ & 1 <= b₁ & b₁ <= len b₅ & 1 < b₂ & b₂ <= width b₅ & 1 <= b₃ & b₃ <= len b₆ & 1 < b₄ & b₄ <= width b₆ & b₅ * b₁,b₂ = b₆ * b₃,b₄ holds
(b₅ * b₁,(b₂ -' 1)) `2 <= (b₆ * b₃,(b₄ -' 1)) `2

proof end;

Lemma15: for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being Matrix of b₃ st 1 <= b₁ & b₁ <= len b₄ & 1 <= b₂ & b₂ <= width b₄ holds
b₄ * b₁,b₂ in Values b₄

proof end;

theorem Th18: :: GOBRD13:18

for b₁, b₂, b₃, b₄ being Nat
for b₅, b₆ being Go-board st Values b₅ c= Values b₆ & [b₁,b₂] in Indices b₅ & [b₃,b₄] in Indices b₆ & b₅ * b₁,b₂ = b₆ * b₃,b₄ holds
cell b₆,b₃,b₄ c= cell b₅,b₁,b₂

proof end;

theorem Th19: :: GOBRD13:19

for b₁, b₂, b₃, b₄ being Nat
for b₅, b₆ being Go-board st Values b₅ c= Values b₆ & [b₁,b₂] in Indices b₅ & [b₃,b₄] in Indices b₆ & b₅ * b₁,b₂ = b₆ * b₃,b₄ holds
cell b₆,(b₃ -' 1),b₄ c= cell b₅,(b₁ -' 1),b₂

proof end;

theorem Th20: :: GOBRD13:20

for b₁, b₂, b₃, b₄ being Nat
for b₅, b₆ being Go-board st Values b₅ c= Values b₆ & [b₁,b₂] in Indices b₅ & [b₃,b₄] in Indices b₆ & b₅ * b₁,b₂ = b₆ * b₃,b₄ holds
cell b₆,b₃,(b₄ -' 1) c= cell b₅,b₁,(b₂ -' 1)

proof end;

Lemma19: for b₁, b₂ being Nat
for b₃ being non empty FinSequence of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (GoB b₃) & 1 <= b₂ & b₂ <= width (GoB b₃) holds
ex b₄ being Nat st
( b₄ in dom b₃ & (b₃ /. b₄) `1 = ((GoB b₃) * b₁,b₂) `1 )

proof end;

Lemma20: for b₁, b₂ being Nat
for b₃ being non empty FinSequence of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (GoB b₃) & 1 <= b₂ & b₂ <= width (GoB b₃) holds
ex b₄ being Nat st
( b₄ in dom b₃ & (b₃ /. b₄) `2 = ((GoB b₃) * b₁,b₂) `2 )

proof end;

theorem Th21: :: GOBRD13:21

for b₁ being Go-board
for b₂ being standard special_circular_sequence st b₂ is_sequence_on b₁ holds
Values (GoB b₂) c= Values b₁

proof end;

definition

let c₁ be FinSequence of (TOP-REAL 2);
let c₂ be Go-board;
let c₃ be Nat;
assume that
E22: ( 1 <= c₃ & c₃ + 1 <= len c₁ ) and
E23: c₁ is_sequence_on c₂ ;
consider c₄, c₅, c₆, c₇ being Nat such that
E24: ( [c₄,c₅] in Indices c₂ & c₁ /. c₃ = c₂ * c₄,c₅ ) and
E25: ( [c₆,c₇] in Indices c₂ & c₁ /. (c₃ + 1) = c₂ * c₆,c₇ ) and
E26: ( ( c₄ = c₆ & c₅ + 1 = c₇ ) or ( c₄ + 1 = c₆ & c₅ = c₇ ) or ( c₄ = c₆ + 1 & c₅ = c₇ ) or ( c₄ = c₆ & c₅ = c₇ + 1 ) ) by E22, E23, JORDAN8:6;
func right_cell c₁,c₃,c₂ -> Subset of (TOP-REAL 2) means :Def2: :: GOBRD13:def 2
for b₁, b₂, b₃, b₄ being Nat st [b₁,b₂] in Indices a₂ & [b₃,b₄] in Indices a₂ & a₁ /. a₃ = a₂ * b₁,b₂ & a₁ /. (a₃ + 1) = a₂ * b₃,b₄ & not ( b₁ = b₃ & b₂ + 1 = b₄ & a₄ = cell a₂,b₁,b₂ ) & not ( b₁ + 1 = b₃ & b₂ = b₄ & a₄ = cell a₂,b₁,(b₂ -' 1) ) & not ( b₁ = b₃ + 1 & b₂ = b₄ & a₄ = cell a₂,b₃,b₄ ) holds
( b₁ = b₃ & b₂ = b₄ + 1 & a₄ = cell a₂,(b₁ -' 1),b₄ );
existence

proof end;

uniqueness

proof end;

func left_cell c₁,c₃,c₂ -> Subset of (TOP-REAL 2) means :Def3: :: GOBRD13:def 3
for b₁, b₂, b₃, b₄ being Nat st [b₁,b₂] in Indices a₂ & [b₃,b₄] in Indices a₂ & a₁ /. a₃ = a₂ * b₁,b₂ & a₁ /. (a₃ + 1) = a₂ * b₃,b₄ & not ( b₁ = b₃ & b₂ + 1 = b₄ & a₄ = cell a₂,(b₁ -' 1),b₂ ) & not ( b₁ + 1 = b₃ & b₂ = b₄ & a₄ = cell a₂,b₁,b₂ ) & not ( b₁ = b₃ + 1 & b₂ = b₄ & a₄ = cell a₂,b₃,(b₄ -' 1) ) holds
( b₁ = b₃ & b₂ = b₄ + 1 & a₄ = cell a₂,b₁,b₄ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines right_cell GOBRD13:def 2 :

:: deftheorem Def3 defines left_cell GOBRD13:def 3 :

theorem Th22: :: GOBRD13:22

for b₁, b₂, b₃ being Nat
for b₄ being FinSequence of (TOP-REAL 2)
for b₅ being Go-board st 1 <= b₁ & b₁ + 1 <= len b₄ & b₄ is_sequence_on b₅ & [b₂,b₃] in Indices b₅ & [b₂,(b₃ + 1)] in Indices b₅ & b₄ /. b₁ = b₅ * b₂,b₃ & b₄ /. (b₁ + 1) = b₅ * b₂,(b₃ + 1) holds
left_cell b₄,b₁,b₅ = cell b₅,(b₂ -' 1),b₃

proof end;

theorem Th23: :: GOBRD13:23

proof end;

theorem Th24: :: GOBRD13:24

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

proof end;

theorem Th25: :: GOBRD13:25

proof end;

theorem Th26: :: GOBRD13:26

for b₁, b₂, b₃ being Nat
for b₄ being FinSequence of (TOP-REAL 2)
for b₅ being Go-board st 1 <= b₁ & b₁ + 1 <= len b₄ & b₄ is_sequence_on b₅ & [b₂,b₃] in Indices b₅ & [(b₂ + 1),b₃] in Indices b₅ & b₄ /. b₁ = b₅ * (b₂ + 1),b₃ & b₄ /. (b₁ + 1) = b₅ * b₂,b₃ holds
left_cell b₄,b₁,b₅ = cell b₅,b₂,(b₃ -' 1)

proof end;

theorem Th27: :: GOBRD13:27

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

proof end;

theorem Th28: :: GOBRD13:28

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

proof end;

theorem Th29: :: GOBRD13:29

proof end;

theorem Th30: :: GOBRD13:30

for b₁ being Nat
for b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Go-board st 1 <= b₁ & b₁ + 1 <= len b₂ & b₂ is_sequence_on b₃ holds
(left_cell b₂,b₁,b₃) /\ (right_cell b₂,b₁,b₃) = LSeg b₂,b₁

proof end;

theorem Th31: :: GOBRD13:31

for b₁ being Nat
for b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Go-board st 1 <= b₁ & b₁ + 1 <= len b₂ & b₂ is_sequence_on b₃ holds
right_cell b₂,b₁,b₃ is closed

proof end;

theorem Th32: :: GOBRD13:32

for b₁, b₂ being Nat
for b₃ being FinSequence of (TOP-REAL 2)
for b₄ being Go-board st 1 <= b₁ & b₁ + 1 <= len b₃ & b₃ is_sequence_on b₄ & b₁ + 1 <= b₂ holds
( left_cell b₃,b₁,b₄ = left_cell (b₃ | b₂),b₁,b₄ & right_cell b₃,b₁,b₄ = right_cell (b₃ | b₂),b₁,b₄ )

proof end;

theorem Th33: :: GOBRD13:33

for b₁, b₂ being Nat
for b₃ being FinSequence of (TOP-REAL 2)
for b₄ being Go-board st 1 <= b₁ & b₁ + 1 <= len (b₃ /^ b₂) & b₂ <= len b₃ & b₃ is_sequence_on b₄ holds
( left_cell b₃,(b₁ + b₂),b₄ = left_cell (b₃ /^ b₂),b₁,b₄ & right_cell b₃,(b₁ + b₂),b₄ = right_cell (b₃ /^ b₂),b₁,b₄ )

proof end;

theorem Th34: :: GOBRD13:34

for b₁ being Nat
for b₂ being Go-board
for b₃ being standard special_circular_sequence st 1 <= b₁ & b₁ + 1 <= len b₃ & b₃ is_sequence_on b₂ holds
( left_cell b₃,b₁,b₂ c= left_cell b₃,b₁ & right_cell b₃,b₁,b₂ c= right_cell b₃,b₁ )

proof end;

definition

let c₁ be FinSequence of (TOP-REAL 2);
let c₂ be Go-board;
let c₃ be Nat;
assume that
E32: ( 1 <= c₃ & c₃ + 1 <= len c₁ ) and
E33: c₁ is_sequence_on c₂ ;
consider c₄, c₅, c₆, c₇ being Nat such that
E34: ( [c₄,c₅] in Indices c₂ & c₁ /. c₃ = c₂ * c₄,c₅ ) and
E35: ( [c₆,c₇] in Indices c₂ & c₁ /. (c₃ + 1) = c₂ * c₆,c₇ ) and
E36: ( ( c₄ = c₆ & c₅ + 1 = c₇ ) or ( c₄ + 1 = c₆ & c₅ = c₇ ) or ( c₄ = c₆ + 1 & c₅ = c₇ ) or ( c₄ = c₆ & c₅ = c₇ + 1 ) ) by E32, E33, JORDAN8:6;
func front_right_cell c₁,c₃,c₂ -> Subset of (TOP-REAL 2) means :Def4: :: GOBRD13:def 4
for b₁, b₂, b₃, b₄ being Nat st [b₁,b₂] in Indices a₂ & [b₃,b₄] in Indices a₂ & a₁ /. a₃ = a₂ * b₁,b₂ & a₁ /. (a₃ + 1) = a₂ * b₃,b₄ & not ( b₁ = b₃ & b₂ + 1 = b₄ & a₄ = cell a₂,b₃,b₄ ) & not ( b₁ + 1 = b₃ & b₂ = b₄ & a₄ = cell a₂,b₃,(b₄ -' 1) ) & not ( b₁ = b₃ + 1 & b₂ = b₄ & a₄ = cell a₂,(b₃ -' 1),b₄ ) holds
( b₁ = b₃ & b₂ = b₄ + 1 & a₄ = cell a₂,(b₃ -' 1),(b₄ -' 1) );
existence

proof end;

uniqueness

proof end;

func front_left_cell c₁,c₃,c₂ -> Subset of (TOP-REAL 2) means :Def5: :: GOBRD13:def 5
for b₁, b₂, b₃, b₄ being Nat st [b₁,b₂] in Indices a₂ & [b₃,b₄] in Indices a₂ & a₁ /. a₃ = a₂ * b₁,b₂ & a₁ /. (a₃ + 1) = a₂ * b₃,b₄ & not ( b₁ = b₃ & b₂ + 1 = b₄ & a₄ = cell a₂,(b₃ -' 1),b₄ ) & not ( b₁ + 1 = b₃ & b₂ = b₄ & a₄ = cell a₂,b₃,b₄ ) & not ( b₁ = b₃ + 1 & b₂ = b₄ & a₄ = cell a₂,(b₃ -' 1),(b₄ -' 1) ) holds
( b₁ = b₃ & b₂ = b₄ + 1 & a₄ = cell a₂,b₃,(b₄ -' 1) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines front_right_cell GOBRD13:def 4 :

:: deftheorem Def5 defines front_left_cell GOBRD13:def 5 :

theorem Th35: :: GOBRD13:35

for b₁, b₂, b₃ being Nat
for b₄ being FinSequence of (TOP-REAL 2)
for b₅ being Go-board st 1 <= b₁ & b₁ + 1 <= len b₄ & b₄ is_sequence_on b₅ & [b₂,b₃] in Indices b₅ & [b₂,(b₃ + 1)] in Indices b₅ & b₄ /. b₁ = b₅ * b₂,b₃ & b₄ /. (b₁ + 1) = b₅ * b₂,(b₃ + 1) holds
front_left_cell b₄,b₁,b₅ = cell b₅,(b₂ -' 1),(b₃ + 1)

proof end;

theorem Th36: :: GOBRD13:36

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

proof end;

theorem Th37: :: GOBRD13:37

proof end;

theorem Th38: :: GOBRD13:38

proof end;

theorem Th39: :: GOBRD13:39

for b₁, b₂, b₃ being Nat
for b₄ being FinSequence of (TOP-REAL 2)
for b₅ being Go-board st 1 <= b₁ & b₁ + 1 <= len b₄ & b₄ is_sequence_on b₅ & [b₂,b₃] in Indices b₅ & [(b₂ + 1),b₃] in Indices b₅ & b₄ /. b₁ = b₅ * (b₂ + 1),b₃ & b₄ /. (b₁ + 1) = b₅ * b₂,b₃ holds
front_left_cell b₄,b₁,b₅ = cell b₅,(b₂ -' 1),(b₃ -' 1)

proof end;

theorem Th40: :: GOBRD13:40

for b₁, b₂, b₃ being Nat
for b₄ being FinSequence of (TOP-REAL 2)
for b₅ being Go-board st 1 <= b₁ & b₁ + 1 <= len b₄ & b₄ is_sequence_on b₅ & [b₂,b₃] in Indices b₅ & [(b₂ + 1),b₃] in Indices b₅ & b₄ /. b₁ = b₅ * (b₂ + 1),b₃ & b₄ /. (b₁ + 1) = b₅ * b₂,b₃ holds
front_right_cell b₄,b₁,b₅ = cell b₅,(b₂ -' 1),b₃

proof end;

theorem Th41: :: GOBRD13:41

proof end;

theorem Th42: :: GOBRD13:42

proof end;

theorem Th43: :: GOBRD13:43

for b₁, b₂ being Nat
for b₃ being FinSequence of (TOP-REAL 2)
for b₄ being Go-board st 1 <= b₁ & b₁ + 1 <= len b₃ & b₃ is_sequence_on b₄ & b₁ + 1 <= b₂ holds
( front_left_cell b₃,b₁,b₄ = front_left_cell (b₃ | b₂),b₁,b₄ & front_right_cell b₃,b₁,b₄ = front_right_cell (b₃ | b₂),b₁,b₄ )

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence of c₁;
let c₃ be Matrix of c₁;
let c₄ be Nat;
pred c₂ turns_right c₄,c₃ means :Def6: :: GOBRD13:def 6
for b₁, b₂, b₃, b₄ being Nat st [b₁,b₂] in Indices a₃ & [b₃,b₄] in Indices a₃ & a₂ /. a₄ = a₃ * b₁,b₂ & a₂ /. (a₄ + 1) = a₃ * b₃,b₄ & not ( b₁ = b₃ & b₂ + 1 = b₄ & [(b₃ + 1),b₄] in Indices a₃ & a₂ /. (a₄ + 2) = a₃ * (b₃ + 1),b₄ ) & not ( b₁ + 1 = b₃ & b₂ = b₄ & [b₃,(b₄ -' 1)] in Indices a₃ & a₂ /. (a₄ + 2) = a₃ * b₃,(b₄ -' 1) ) & not ( b₁ = b₃ + 1 & b₂ = b₄ & [b₃,(b₄ + 1)] in Indices a₃ & a₂ /. (a₄ + 2) = a₃ * b₃,(b₄ + 1) ) holds
( b₁ = b₃ & b₂ = b₄ + 1 & [(b₃ -' 1),b₄] in Indices a₃ & a₂ /. (a₄ + 2) = a₃ * (b₃ -' 1),b₄ );
pred c₂ turns_left c₄,c₃ means :Def7: :: GOBRD13:def 7
for b₁, b₂, b₃, b₄ being Nat st [b₁,b₂] in Indices a₃ & [b₃,b₄] in Indices a₃ & a₂ /. a₄ = a₃ * b₁,b₂ & a₂ /. (a₄ + 1) = a₃ * b₃,b₄ & not ( b₁ = b₃ & b₂ + 1 = b₄ & [(b₃ -' 1),b₄] in Indices a₃ & a₂ /. (a₄ + 2) = a₃ * (b₃ -' 1),b₄ ) & not ( b₁ + 1 = b₃ & b₂ = b₄ & [b₃,(b₄ + 1)] in Indices a₃ & a₂ /. (a₄ + 2) = a₃ * b₃,(b₄ + 1) ) & not ( b₁ = b₃ + 1 & b₂ = b₄ & [b₃,(b₄ -' 1)] in Indices a₃ & a₂ /. (a₄ + 2) = a₃ * b₃,(b₄ -' 1) ) holds
( b₁ = b₃ & b₂ = b₄ + 1 & [(b₃ + 1),b₄] in Indices a₃ & a₂ /. (a₄ + 2) = a₃ * (b₃ + 1),b₄ );
pred c₂ goes_straight c₄,c₃ means :Def8: :: GOBRD13:def 8
for b₁, b₂, b₃, b₄ being Nat st [b₁,b₂] in Indices a₃ & [b₃,b₄] in Indices a₃ & a₂ /. a₄ = a₃ * b₁,b₂ & a₂ /. (a₄ + 1) = a₃ * b₃,b₄ & not ( b₁ = b₃ & b₂ + 1 = b₄ & [b₃,(b₄ + 1)] in Indices a₃ & a₂ /. (a₄ + 2) = a₃ * b₃,(b₄ + 1) ) & not ( b₁ + 1 = b₃ & b₂ = b₄ & [(b₃ + 1),b₄] in Indices a₃ & a₂ /. (a₄ + 2) = a₃ * (b₃ + 1),b₄ ) & not ( b₁ = b₃ + 1 & b₂ = b₄ & [(b₃ -' 1),b₄] in Indices a₃ & a₂ /. (a₄ + 2) = a₃ * (b₃ -' 1),b₄ ) holds
( b₁ = b₃ & b₂ = b₄ + 1 & [b₃,(b₄ -' 1)] in Indices a₃ & a₂ /. (a₄ + 2) = a₃ * b₃,(b₄ -' 1) );

end;

:: deftheorem Def6 defines turns_right GOBRD13:def 6 :

:: deftheorem Def7 defines turns_left GOBRD13:def 7 :

:: deftheorem Def8 defines goes_straight GOBRD13:def 8 :

theorem Th44: :: GOBRD13:44

for b₁, b₂ being Nat
for b₃ being set
for b₄ being FinSequence of b₃
for b₅ being Matrix of b₃ st 1 <= b₁ & b₁ + 2 <= len b₄ & b₁ + 2 <= b₂ & b₄ | b₂ turns_right b₁,b₅ holds
b₄ turns_right b₁,b₅

proof end;

theorem Th45: :: GOBRD13:45

for b₁, b₂ being Nat
for b₃ being set
for b₄ being FinSequence of b₃
for b₅ being Matrix of b₃ st 1 <= b₁ & b₁ + 2 <= len b₄ & b₁ + 2 <= b₂ & b₄ | b₂ turns_left b₁,b₅ holds
b₄ turns_left b₁,b₅

proof end;

theorem Th46: :: GOBRD13:46

for b₁, b₂ being Nat
for b₃ being set
for b₄ being FinSequence of b₃
for b₅ being Matrix of b₃ st 1 <= b₁ & b₁ + 2 <= len b₄ & b₁ + 2 <= b₂ & b₄ | b₂ goes_straight b₁,b₅ holds
b₄ goes_straight b₁,b₅

proof end;

theorem Th47: :: GOBRD13:47

for b₁ being Nat
for b₂ being set
for b₃, b₄ being FinSequence of b₂
for b₅ being Matrix of b₂ st 1 < b₁ & b₁ + 1 <= len b₃ & b₁ + 1 <= len b₄ & b₃ is_sequence_on b₅ & b₃ | b₁ = b₄ | b₁ & b₃ turns_right b₁ -' 1,b₅ & b₄ turns_right b₁ -' 1,b₅ holds
b₃ | (b₁ + 1) = b₄ | (b₁ + 1)

proof end;

theorem Th48: :: GOBRD13:48

for b₁ being Nat
for b₂ being set
for b₃, b₄ being FinSequence of b₂
for b₅ being Matrix of b₂ st 1 < b₁ & b₁ + 1 <= len b₃ & b₁ + 1 <= len b₄ & b₃ is_sequence_on b₅ & b₃ | b₁ = b₄ | b₁ & b₃ turns_left b₁ -' 1,b₅ & b₄ turns_left b₁ -' 1,b₅ holds
b₃ | (b₁ + 1) = b₄ | (b₁ + 1)

proof end;

theorem Th49: :: GOBRD13:49

for b₁ being Nat
for b₂ being set
for b₃, b₄ being FinSequence of b₂
for b₅ being Matrix of b₂ st 1 < b₁ & b₁ + 1 <= len b₃ & b₁ + 1 <= len b₄ & b₃ is_sequence_on b₅ & b₃ | b₁ = b₄ | b₁ & b₃ goes_straight b₁ -' 1,b₅ & b₄ goes_straight b₁ -' 1,b₅ holds
b₃ | (b₁ + 1) = b₄ | (b₁ + 1)

proof end;

theorem Th50: :: GOBRD13:50

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being Matrix of b₃ st 1 <= b₁ & b₁ <= len b₄ & 1 <= b₂ & b₂ <= width b₄ holds
b₄ * b₁,b₂ in Values b₄ by Lemma15;