:: Properties of Go-Board - Part III
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Received August 24, 1992
:: Copyright (c) 1992 Association of Mizar Users
Lm1:
now
let f be
FinSequence of
(TOP-REAL 2);
:: thesis: for k being Element of NAT st len f = k + 1 & k <> 0 & f is unfolded holds
f | k is unfolded let k be
Element of
NAT ;
:: thesis: ( len f = k + 1 & k <> 0 & f is unfolded implies f | k is unfolded )assume A1:
len f = k + 1
;
:: thesis: ( k <> 0 & f is unfolded implies f | k is unfolded )assume
k <> 0
;
:: thesis: ( f is unfolded implies f | k is unfolded )then A2:
(
0 < k &
k <= k + 1 )
by NAT_1:11;
then
(
0 + 1
<= k &
k <= len f &
k + 1
<= len f )
by A1, NAT_1:13;
then A3:
k in dom f
by FINSEQ_3:27;
A4:
len (f | k) = k
by A1, FINSEQ_1:80, NAT_1:11;
A5:
dom (f | k) = Seg (len (f | k))
by FINSEQ_1:def 3;
assume A6:
f is
unfolded
;
:: thesis: f | k is unfolded thus
f | k is
unfolded
:: thesis: verum
proof
set f1 =
f | k;
let n be
Nat;
:: according to TOPREAL1:def 8 :: thesis: ( not 1 <= n or not n + 2 <= len (f | k) or (LSeg (f | k),n) /\ (LSeg (f | k),(n + 1)) = {((f | k) /. (n + 1))} )
assume A7:
( 1
<= n &
n + 2
<= len (f | k) )
;
:: thesis: (LSeg (f | k),n) /\ (LSeg (f | k),(n + 1)) = {((f | k) /. (n + 1))}
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
(
n in dom (f | k) &
n + 1
in dom (f | k) &
n + 2
in dom (f | k) &
(n + 1) + 1
= n + (1 + 1) )
by A7, GOBOARD2:4;
then A8:
(
LSeg (f | k),
n = LSeg f,
n &
LSeg (f | k),
(n + 1) = LSeg f,
(n + 1) &
(f | k) /. (n + 1) = f /. (n + 1) )
by A3, A4, A5, FINSEQ_4:86, TOPREAL3:24;
len (f | k) <= len f
by A1, A2, FINSEQ_1:80;
then
n + 2
<= len f
by A7, XXREAL_0:2;
hence
(LSeg (f | k),n) /\ (LSeg (f | k),(n + 1)) = {((f | k) /. (n + 1))}
by A6, A7, A8, TOPREAL1:def 8;
:: thesis: verum
end;
end;
theorem Th1: :: GOBOARD3:1
theorem :: GOBOARD3:2