:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura

::

:: Received August 24, 1992

:: Copyright (c) 1992-2021 Association of Mizar Users

Lm1: now :: thesis: for f being FinSequence of (TOP-REAL 2)

for k being Nat st len f = k + 1 & k <> 0 & f is unfolded holds

f | k is unfolded

for k being Nat st len f = k + 1 & k <> 0 & f is unfolded holds

f | k is unfolded

let f be FinSequence of (TOP-REAL 2); :: thesis: for k being Nat st len f = k + 1 & k <> 0 & f is unfolded holds

f | k is unfolded

let k be Nat; :: thesis: ( len f = k + 1 & k <> 0 & f is unfolded implies f | k is unfolded )

A1: dom (f | k) = Seg (len (f | k)) by FINSEQ_1:def 3;

assume A2: len f = k + 1 ; :: thesis: ( k <> 0 & f is unfolded implies f | k is unfolded )

then A3: len (f | k) = k by FINSEQ_1:59, NAT_1:11;

assume k <> 0 ; :: thesis: ( f is unfolded implies f | k is unfolded )

then A4: 0 + 1 <= k by NAT_1:13;

assume A5: f is unfolded ; :: thesis: f | k is unfolded

A6: k <= k + 1 by NAT_1:11;

then A7: k in dom f by A2, A4, FINSEQ_3:25;

thus f | k is unfolded :: thesis: verum

end;
f | k is unfolded

let k be Nat; :: thesis: ( len f = k + 1 & k <> 0 & f is unfolded implies f | k is unfolded )

A1: dom (f | k) = Seg (len (f | k)) by FINSEQ_1:def 3;

assume A2: len f = k + 1 ; :: thesis: ( k <> 0 & f is unfolded implies f | k is unfolded )

then A3: len (f | k) = k by FINSEQ_1:59, NAT_1:11;

assume k <> 0 ; :: thesis: ( f is unfolded implies f | k is unfolded )

then A4: 0 + 1 <= k by NAT_1:13;

assume A5: f is unfolded ; :: thesis: f | k is unfolded

A6: k <= k + 1 by NAT_1:11;

then A7: k in dom f by A2, A4, FINSEQ_3:25;

thus f | k is unfolded :: thesis: verum

proof

let n be Nat; :: according to TOPREAL1:def 6 :: 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))} )

set f1 = f | k;

assume that

A8: 1 <= n and

A9: 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 12;

A10: n + 1 in dom (f | k) by A8, A9, SEQ_4:135;

n in dom (f | k) by A8, A9, SEQ_4:135;

then A11: LSeg ((f | k),n) = LSeg (f,n) by A10, TOPREAL3:17;

len (f | k) <= len f by A2, A6, FINSEQ_1:59;

then A12: n + 2 <= len f by A9, XXREAL_0:2;

A13: (n + 1) + 1 = n + (1 + 1) ;

n + 2 in dom (f | k) by A8, A9, SEQ_4:135;

then A14: LSeg ((f | k),(n + 1)) = LSeg (f,(n + 1)) by A10, A13, TOPREAL3:17;

(f | k) /. (n + 1) = f /. (n + 1) by A7, A3, A1, A10, FINSEQ_4:71;

hence (LSeg ((f | k),n)) /\ (LSeg ((f | k),(n + 1))) = {((f | k) /. (n + 1))} by A5, A8, A11, A14, A12; :: thesis: verum

end;
set f1 = f | k;

assume that

A8: 1 <= n and

A9: 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 12;

A10: n + 1 in dom (f | k) by A8, A9, SEQ_4:135;

n in dom (f | k) by A8, A9, SEQ_4:135;

then A11: LSeg ((f | k),n) = LSeg (f,n) by A10, TOPREAL3:17;

len (f | k) <= len f by A2, A6, FINSEQ_1:59;

then A12: n + 2 <= len f by A9, XXREAL_0:2;

A13: (n + 1) + 1 = n + (1 + 1) ;

n + 2 in dom (f | k) by A8, A9, SEQ_4:135;

then A14: LSeg ((f | k),(n + 1)) = LSeg (f,(n + 1)) by A10, A13, TOPREAL3:17;

(f | k) /. (n + 1) = f /. (n + 1) by A7, A3, A1, A10, FINSEQ_4:71;

hence (LSeg ((f | k),n)) /\ (LSeg ((f | k),(n + 1))) = {((f | k) /. (n + 1))} by A5, A8, A11, A14, A12; :: thesis: verum

theorem Th1: :: GOBOARD3:1

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is one-to-one & f is unfolded & f is s.n.c. & f is special holds

ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & g is one-to-one & g is unfolded & g is s.n.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )

for G being Go-board st ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is one-to-one & f is unfolded & f is s.n.c. & f is special holds

ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & g is one-to-one & g is unfolded & g is s.n.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )

proof end;

theorem :: GOBOARD3:2

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is being_S-Seq holds

ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & g is being_S-Seq & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )

for G being Go-board st ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is being_S-Seq holds

ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & g is being_S-Seq & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )

proof end;