:: GOBRD10 semantic presentation

definition
let c1, c2 be Nat;
pred c1,c2 are_adjacent1 means :Def1: :: GOBRD10:def 1
( a2 = a1 + 1 or a1 = a2 + 1 );
symmetry
for b1, b2 being Nat holds
( ( not b2 = b1 + 1 & not b1 = b2 + 1 ) or b1 = b2 + 1 or b2 = b1 + 1 ) ;
irreflexivity
for b1 being Nat holds
( not b1 = b1 + 1 & not b1 = b1 + 1 ) ;
end;

:: deftheorem Def1 defines are_adjacent1 GOBRD10:def 1 :
for b1, b2 being Nat holds
( b1,b2 are_adjacent1 iff ( b2 = b1 + 1 or b1 = b2 + 1 ) );

theorem Th1: :: GOBRD10:1
for b1, b2 being Nat st b1,b2 are_adjacent1 holds
b1 + 1,b2 + 1 are_adjacent1
proof end;

theorem Th2: :: GOBRD10:2
for b1, b2 being Nat st b1,b2 are_adjacent1 & 1 <= b1 & 1 <= b2 holds
b1 -' 1,b2 -' 1 are_adjacent1
proof end;

definition
let c1, c2, c3, c4 be Nat;
pred c1,c2,c3,c4 are_adjacent2 means :Def2: :: GOBRD10:def 2
( ( a1,a3 are_adjacent1 & a2 = a4 ) or ( a1 = a3 & a2,a4 are_adjacent1 ) );
end;

:: deftheorem Def2 defines are_adjacent2 GOBRD10:def 2 :
for b1, b2, b3, b4 being Nat holds
( b1,b2,b3,b4 are_adjacent2 iff ( ( b1,b3 are_adjacent1 & b2 = b4 ) or ( b1 = b3 & b2,b4 are_adjacent1 ) ) );

theorem Th3: :: GOBRD10:3
for b1, b2, b3, b4 being Nat st b1,b3,b2,b4 are_adjacent2 holds
b1 + 1,b3 + 1,b2 + 1,b4 + 1 are_adjacent2
proof end;

theorem Th4: :: GOBRD10:4
for b1, b2, b3, b4 being Nat st b1,b3,b2,b4 are_adjacent2 & 1 <= b1 & 1 <= b2 & 1 <= b3 & 1 <= b4 holds
b1 -' 1,b3 -' 1,b2 -' 1,b4 -' 1 are_adjacent2
proof end;

definition
let c1, c2 be Nat;
redefine func |-> as c1 |-> c2 -> FinSequence of NAT means :Def3: :: GOBRD10:def 3
( len a3 = a1 & ( for b1 being Nat st 1 <= b1 & b1 <= a1 holds
a3 . b1 = a2 ) );
coherence
c1 |-> c2 is FinSequence of NAT by FINSEQ_2:77;
compatibility
for b1 being FinSequence of NAT holds
( b1 = c1 |-> c2 iff ( len b1 = c1 & ( for b2 being Nat st 1 <= b2 & b2 <= c1 holds
b1 . b2 = c2 ) ) )
proof end;
end;

:: deftheorem Def3 defines |-> GOBRD10:def 3 :
for b1, b2 being Nat
for b3 being FinSequence of NAT holds
( b3 = b1 |-> b2 iff ( len b3 = b1 & ( for b4 being Nat st 1 <= b4 & b4 <= b1 holds
b3 . b4 = b2 ) ) );

theorem Th5: :: GOBRD10:5
canceled;

theorem Th6: :: GOBRD10:6
for b1, b2, b3 being Nat st b2 <= b1 & b3 <= b1 holds
ex b4 being FinSequence of NAT st
( b4 . 1 = b2 & b4 . (len b4) = b3 & len b4 = ((b2 -' b3) + (b3 -' b2)) + 1 & ( for b5, b6 being Nat st 1 <= b5 & b5 <= len b4 & b6 = b4 . b5 holds
b6 <= b1 ) & ( for b5 being Nat st 1 <= b5 & b5 < len b4 & not b4 . (b5 + 1) = (b4 /. b5) + 1 holds
b4 . b5 = (b4 /. (b5 + 1)) + 1 ) )
proof end;

theorem Th7: :: GOBRD10:7
for b1, b2, b3 being Nat st b2 <= b1 & b3 <= b1 holds
ex b4 being FinSequence of NAT st
( b4 . 1 = b2 & b4 . (len b4) = b3 & len b4 = ((b2 -' b3) + (b3 -' b2)) + 1 & ( for b5, b6 being Nat st 1 <= b5 & b5 <= len b4 & b6 = b4 . b5 holds
b6 <= b1 ) & ( for b5 being Nat st 1 <= b5 & b5 < len b4 holds
b4 /. b5,b4 /. (b5 + 1) are_adjacent1 ) )
proof end;

theorem Th8: :: GOBRD10:8
for b1, b2, b3, b4, b5, b6 being Nat st b3 <= b1 & b4 <= b2 & b5 <= b1 & b6 <= b2 holds
ex b7, b8 being FinSequence of NAT st
( ( for b9, b10, b11 being Nat st b9 in dom b7 & b10 = b7 . b9 & b11 = b8 . b9 holds
( b10 <= b1 & b11 <= b2 ) ) & b7 . 1 = b3 & b7 . (len b7) = b5 & b8 . 1 = b4 & b8 . (len b8) = b6 & len b7 = len b8 & len b7 = ((((b3 -' b5) + (b5 -' b3)) + (b4 -' b6)) + (b6 -' b4)) + 1 & ( for b9 being Nat st 1 <= b9 & b9 < len b7 holds
b7 /. b9,b8 /. b9,b7 /. (b9 + 1),b8 /. (b9 + 1) are_adjacent2 ) )
proof end;

theorem Th9: :: GOBRD10:9
for b1, b2 being Nat
for b3 being set
for b4 being Subset of b3
for b5 being Matrix of b1,b2, bool b3 st ex b6, b7 being Nat st
( b6 in Seg b1 & b7 in Seg b2 & b5 * b6,b7 c= b4 ) & ( for b6, b7, b8, b9 being Nat st b6 in Seg b1 & b8 in Seg b1 & b7 in Seg b2 & b9 in Seg b2 & b6,b7,b8,b9 are_adjacent2 holds
( b5 * b6,b7 c= b4 iff b5 * b8,b9 c= b4 ) ) holds
for b6, b7 being Nat st b6 in Seg b1 & b7 in Seg b2 holds
b5 * b6,b7 c= b4
proof end;