let f be FinSequence of (TOP-REAL 2); ( f is nodic & PairF f is Simple & f . 1 <> f . (len f) implies f is unfolded )
assume that
A1:
f is nodic
and
A2:
( PairF f is Simple & f . 1 <> f . (len f) )
; f is unfolded
per cases
( 2 < len f or len f <= 2 )
;
suppose A3:
2
< len f
;
f is unfolded then A4:
2
+ 1
<= len f
by NAT_1:13;
then A5:
2
+ 1
in dom f
by FINSEQ_3:25;
A6:
f . 2
= f /. 2
by A3, FINSEQ_4:15;
then A7:
f . 2
in LSeg (
f,2)
by A4, TOPREAL1:21;
1
+ 1
<= len f
by A3;
then
f . 2
in LSeg (
f,1)
by A6, TOPREAL1:21;
then
(LSeg (f,1)) /\ (LSeg (f,2)) <> {}
by A7, XBOOLE_0:def 4;
then A8:
LSeg (
f,1)
meets LSeg (
f,2)
;
A9:
len f < (len f) + 1
by NAT_1:13;
then A10:
(len f) - 1
< len f
by XREAL_1:19;
A11:
2
in dom f
by A3, FINSEQ_3:25;
A12:
LSeg (
f,1)
= LSeg (
(f /. 1),
(f /. (1 + 1)))
by A3, TOPREAL1:def 3;
A13:
f is
one-to-one
by A2, Th18;
A14:
1
< len f
by A3, XXREAL_0:2;
then A15:
1
in dom f
by FINSEQ_3:25;
A16:
f . 1
= f /. 1
by A14, FINSEQ_4:15;
A17:
(len f) -' 2
= (len f) - 2
by A3, XREAL_1:233;
A18:
LSeg (
f,2)
= LSeg (
(f /. 2),
(f /. (2 + 1)))
by A4, TOPREAL1:def 3;
now not LSeg (f,1) = LSeg (f,2)assume A19:
LSeg (
f,1)
= LSeg (
f,2)
;
contradictionnow ( ( f /. 1 = f /. 2 & f /. (1 + 1) = f /. (2 + 1) & contradiction ) or ( f /. 1 = f /. (2 + 1) & f /. (1 + 1) = f /. 2 & contradiction ) )end; hence
contradiction
;
verum end; then
( (
(LSeg (f,1)) /\ (LSeg (f,2)) = {(f . 1)} & (
f . 1
= f . 2 or
f . 1
= f . (2 + 1) ) ) or (
(LSeg (f,1)) /\ (LSeg (f,2)) = {(f . (1 + 1))} & (
f . (1 + 1) = f . 2 or
f . (1 + 1) = f . (2 + 1) ) ) )
by A1, A8;
then A22:
(LSeg (f,1)) /\ (LSeg (f,(1 + 1))) c= {(f /. (1 + 1))}
by A3, A13, A15, A5, FINSEQ_4:15;
A23:
(len f) - 1
= (len f) -' 1
by A3, XREAL_1:233, XXREAL_0:2;
then A24:
((len f) -' 1) + 1
in dom f
by A14, FINSEQ_3:25;
A25:
(1 + 1) - 1
<= (len f) - 1
by A3, XREAL_1:9;
then A26:
f . ((len f) -' 1) = f /. ((len f) -' 1)
by A23, A10, FINSEQ_4:15;
A27:
(2 + 1) - 2
<= (len f) - 2
by A4, XREAL_1:9;
then A28:
LSeg (
f,
((len f) -' 2))
= LSeg (
(f /. ((len f) -' 2)),
(f /. (((len f) -' 2) + 1)))
by A17, A10, TOPREAL1:def 3;
A29:
((len f) - 1) - 1
< (len f) - 1
by A10, XREAL_1:9;
then
(len f) - 2
< len f
by A10, XXREAL_0:2;
then A30:
f . ((len f) -' 2) = f /. ((len f) -' 2)
by A27, A17, FINSEQ_4:15;
A31:
(len f) -' 2
< len f
by A17, A10, A29, XXREAL_0:2;
then A32:
(len f) -' 2
in dom f
by A27, A17, FINSEQ_3:25;
A33:
LSeg (
f,
((len f) -' 1))
= LSeg (
(f /. ((len f) -' 1)),
(f /. (((len f) -' 1) + 1)))
by A25, A23, TOPREAL1:def 3;
A34:
f . ((len f) -' 2) = f /. ((len f) -' 2)
by A27, A17, A31, FINSEQ_4:15;
A35:
now not LSeg (f,((len f) -' 2)) = LSeg (f,((len f) -' 1))assume A36:
LSeg (
f,
((len f) -' 2))
= LSeg (
f,
((len f) -' 1))
;
contradictionA37:
(len f) -' 2
in dom f
by A27, A17, A31, FINSEQ_3:25;
A38:
(len f) -' 1
in dom f
by A25, A23, A10, FINSEQ_3:25;
now ( ( f /. ((len f) -' 2) = f /. ((len f) -' 1) & f /. (((len f) -' 2) + 1) = f /. (((len f) -' 1) + 1) & contradiction ) or ( f /. ((len f) -' 2) = f /. (((len f) -' 1) + 1) & f /. (((len f) -' 2) + 1) = f /. ((len f) -' 1) & contradiction ) )per cases
( ( f /. ((len f) -' 2) = f /. ((len f) -' 1) & f /. (((len f) -' 2) + 1) = f /. (((len f) -' 1) + 1) ) or ( f /. ((len f) -' 2) = f /. (((len f) -' 1) + 1) & f /. (((len f) -' 2) + 1) = f /. ((len f) -' 1) ) )
by A28, A33, A36, SPPOL_1:8;
case A39:
(
f /. ((len f) -' 2) = f /. ((len f) -' 1) &
f /. (((len f) -' 2) + 1) = f /. (((len f) -' 1) + 1) )
;
contradiction
f . ((len f) -' 1) = f /. ((len f) -' 1)
by A25, A23, A10, FINSEQ_4:15;
hence
contradiction
by A13, A23, A17, A9, A34, A37, A38, A39;
verum end; case A40:
(
f /. ((len f) -' 2) = f /. (((len f) -' 1) + 1) &
f /. (((len f) -' 2) + 1) = f /. ((len f) -' 1) )
;
contradiction
((len f) -' 1) + 1
in Seg (len f)
by A14, A23, FINSEQ_1:1;
then A41:
((len f) -' 1) + 1
in dom f
by FINSEQ_1:def 3;
f . (((len f) -' 1) + 1) = f /. (((len f) -' 1) + 1)
by A14, A23, FINSEQ_4:15;
hence
contradiction
by A13, A23, A17, A10, A29, A30, A37, A40, A41;
verum end; end; end; hence
contradiction
;
verum end;
((len f) -' 1) + 1
= len f
by A23;
then A42:
f . ((len f) -' 1) in LSeg (
f,
((len f) -' 1))
by A25, A26, TOPREAL1:21;
((len f) -' 2) + 1
= (len f) - ((1 + 1) - 1)
by A17;
then
f . ((len f) -' 1) in LSeg (
f,
((len f) -' 2))
by A27, A23, A10, A26, TOPREAL1:21;
then
(LSeg (f,((len f) -' 2))) /\ (LSeg (f,((len f) -' 1))) <> {}
by A42, XBOOLE_0:def 4;
then
LSeg (
f,
((len f) -' 2))
meets LSeg (
f,
((len f) -' 1))
;
then
( (
(LSeg (f,((len f) -' 2))) /\ (LSeg (f,((len f) -' 1))) = {(f . ((len f) -' 2))} & (
f . ((len f) -' 2) = f . ((len f) -' 1) or
f . ((len f) -' 2) = f . (((len f) -' 1) + 1) ) ) or (
(LSeg (f,((len f) -' 2))) /\ (LSeg (f,((len f) -' 1))) = {(f . (((len f) -' 2) + 1))} & (
f . (((len f) -' 2) + 1) = f . ((len f) -' 1) or
f . (((len f) -' 2) + 1) = f . (((len f) -' 1) + 1) ) ) )
by A1, A35;
then
(LSeg (f,((len f) -' 2))) /\ (LSeg (f,((len f) -' 1))) c= {(f /. ((len f) -' 1))}
by A13, A25, A23, A17, A10, A29, A32, A24, FINSEQ_4:15;
hence
f is
unfolded
by A1, A2, A22, Th15, Th17;
verum end; end;