:: GOBRD10 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let i1, i2 be Nat;
pred i1,i2 are_adjacent1 means :Def1: :: GOBRD10:def 1
( i2 = i1 + 1 or i1 = i2 + 1 );
symmetry
for i1, i2 being Nat holds
( ( not i2 = i1 + 1 & not i1 = i2 + 1 ) or i1 = i2 + 1 or i2 = i1 + 1 ) ;
irreflexivity
for i1 being Nat holds
( not i1 = i1 + 1 & not i1 = i1 + 1 ) ;
end;

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

theorem Th1: :: GOBRD10:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2 being Nat st i1,i2 are_adjacent1 holds
i1 + 1,i2 + 1 are_adjacent1
proof end;

theorem Th2: :: GOBRD10:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2 being Nat st i1,i2 are_adjacent1 & 1 <= i1 & 1 <= i2 holds
i1 -' 1,i2 -' 1 are_adjacent1
proof end;

definition
let i1, j1, i2, j2 be Nat;
pred i1,j1,i2,j2 are_adjacent2 means :Def2: :: GOBRD10:def 2
( ( i1,i2 are_adjacent1 & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent1 ) );
end;

:: deftheorem Def2 defines are_adjacent2 GOBRD10:def 2 :
for i1, j1, i2, j2 being Nat holds
( i1,j1,i2,j2 are_adjacent2 iff ( ( i1,i2 are_adjacent1 & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent1 ) ) );

theorem Th3: :: GOBRD10:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2, j1, j2 being Nat st i1,j1,i2,j2 are_adjacent2 holds
i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent2
proof end;

theorem :: GOBRD10:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2, j1, j2 being Nat st i1,j1,i2,j2 are_adjacent2 & 1 <= i1 & 1 <= i2 & 1 <= j1 & 1 <= j2 holds
i1 -' 1,j1 -' 1,i2 -' 1,j2 -' 1 are_adjacent2
proof end;

definition
let n, i be Nat;
:: original: |->
redefine func n |-> i -> FinSequence of NAT means :Def3: :: GOBRD10:def 3
( len it = n & ( for j being Nat st 1 <= j & j <= n holds
it . j = i ) );
coherence
n |-> i is FinSequence of NAT by FINSEQ_2:77;
compatibility
for b1 being FinSequence of NAT holds
( b1 = n |-> i iff ( len b1 = n & ( for j being Nat st 1 <= j & j <= n holds
b1 . j = i ) ) )
proof end;
end;

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

theorem :: GOBRD10:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th6: :: GOBRD10:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i, j being Nat st i <= n & j <= n holds
ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Nat st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Nat st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds
fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )
proof end;

theorem Th7: :: GOBRD10:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i, j being Nat st i <= n & j <= n holds
ex fs1 being FinSequence of NAT st
( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Nat st 1 <= k & k <= len fs1 & k1 = fs1 . k holds
k1 <= n ) & ( for i1 being Nat st 1 <= i1 & i1 < len fs1 holds
fs1 /. i1,fs1 /. (i1 + 1) are_adjacent1 ) )
proof end;

theorem Th8: :: GOBRD10:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m, i1, j1, i2, j2 being Nat st i1 <= n & j1 <= m & i2 <= n & j2 <= m holds
ex fs1, fs2 being FinSequence of NAT st
( ( for i, k1, k2 being Nat st i in dom fs1 & k1 = fs1 . i & k2 = fs2 . i holds
( k1 <= n & k2 <= m ) ) & fs1 . 1 = i1 & fs1 . (len fs1) = i2 & fs2 . 1 = j1 & fs2 . (len fs2) = j2 & len fs1 = len fs2 & len fs1 = ((((i1 -' i2) + (i2 -' i1)) + (j1 -' j2)) + (j2 -' j1)) + 1 & ( for i being Nat st 1 <= i & i < len fs1 holds
fs1 /. i,fs2 /. i,fs1 /. (i + 1),fs2 /. (i + 1) are_adjacent2 ) )
proof end;

theorem :: GOBRD10:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat
for S being set
for Y being Subset of S
for F being Matrix of n,m, bool S st ex i, j being Nat st
( i in Seg n & j in Seg m & F * i,j c= Y ) & ( for i1, j1, i2, j2 being Nat st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent2 holds
( F * i1,j1 c= Y iff F * i2,j2 c= Y ) ) holds
for i, j being Nat st i in Seg n & j in Seg m holds
F * i,j c= Y
proof end;