let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is nodic & PairF f is Simple implies f is s.c.c. )
assume that
A1: f is nodic and
A2: PairF f is Simple ; :: thesis: f is s.c.c.
reconsider f1 = f as FinSequence of the carrier of (PGraph the carrier of (TOP-REAL 2)) ;
per cases ( len f >= 1 or len f < 1 ) ;
suppose len f >= 1 ; :: thesis: f is s.c.c.
then A3: f1 is_oriented_vertex_seq_of PairF f by Th11;
for i, j being Element of NAT st i + 1 < j & ( ( i > 1 & j < len f ) or j + 1 < len f ) holds
LSeg f,i misses LSeg f,j
proof
let i, j be Element of NAT ; :: thesis: ( i + 1 < j & ( ( i > 1 & j < len f ) or j + 1 < len f ) implies LSeg f,i misses LSeg f,j )
assume that
A4: i + 1 < j and
A5: ( ( i > 1 & j < len f ) or j + 1 < len f ) ; :: thesis: LSeg f,i misses LSeg f,j
per cases ( i >= 1 or i < 1 ) ;
suppose A6: i >= 1 ; :: thesis: LSeg f,i misses LSeg f,j
A7: i < j by A4, NAT_1:13;
then A8: 1 <= j by A6, XXREAL_0:2;
then A9: 1 < j + 1 by NAT_1:13;
A10: i + 1 < j + 1 by A4, NAT_1:13;
A11: 1 < i + 1 by A6, NAT_1:13;
A12: j < len f by A5, NAT_1:13;
then A13: i + 1 < len f by A4, XXREAL_0:2;
A14: j + 1 <= len f by A5, NAT_1:13;
A15: i < j + 1 by A7, NAT_1:13;
then A16: i < len f by A14, XXREAL_0:2;
now
assume A17: LSeg f,i meets LSeg f,j ; :: thesis: contradiction
now
per cases ( ( (LSeg f,i) /\ (LSeg f,j) = {(f . i)} & ( f . i = f . j or f . i = f . (j + 1) ) & LSeg f,i <> LSeg f,j ) or ( (LSeg f,i) /\ (LSeg f,j) = {(f . (i + 1))} & ( f . (i + 1) = f . j or f . (i + 1) = f . (j + 1) ) & LSeg f,i <> LSeg f,j ) or LSeg f,i = LSeg f,j ) by A1, A17, Def4;
case A18: ( (LSeg f,i) /\ (LSeg f,j) = {(f . i)} & ( f . i = f . j or f . i = f . (j + 1) ) & LSeg f,i <> LSeg f,j ) ; :: thesis: contradiction
now
per cases ( f . i = f . j or f . i = f . (j + 1) ) by A18;
case f . i = f . j ; :: thesis: contradiction
hence contradiction by A2, A3, A6, A7, A12, Th4; :: thesis: verum
end;
case f . i = f . (j + 1) ; :: thesis: contradiction
hence contradiction by A2, A3, A5, A6, A15, A14, Th4; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
case A19: ( (LSeg f,i) /\ (LSeg f,j) = {(f . (i + 1))} & ( f . (i + 1) = f . j or f . (i + 1) = f . (j + 1) ) & LSeg f,i <> LSeg f,j ) ; :: thesis: contradiction
now
per cases ( f . (i + 1) = f . j or f . (i + 1) = f . (j + 1) ) by A19;
case f . (i + 1) = f . j ; :: thesis: contradiction
hence contradiction by A2, A3, A4, A12, A11, Th4; :: thesis: verum
end;
case f . (i + 1) = f . (j + 1) ; :: thesis: contradiction
hence contradiction by A2, A3, A10, A14, A11, Th4; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
case LSeg f,i = LSeg f,j ; :: thesis: contradiction
then LSeg (f /. i),(f /. (i + 1)) = LSeg f,j by A6, A13, TOPREAL1:def 5;
then A20: LSeg (f /. i),(f /. (i + 1)) = LSeg (f /. j),(f /. (j + 1)) by A8, A14, TOPREAL1:def 5;
A21: ( f /. j = f . j & f /. (j + 1) = f . (j + 1) ) by A8, A12, A14, A9, FINSEQ_4:24;
A22: ( f /. i = f . i & f /. (i + 1) = f . (i + 1) ) by A6, A13, A16, A11, FINSEQ_4:24;
now
per cases ( ( f . i = f . j & f . (i + 1) = f . (j + 1) ) or ( f . i = f . (j + 1) & f . (i + 1) = f . j ) ) by A20, A22, A21, SPPOL_1:25;
case ( f . i = f . j & f . (i + 1) = f . (j + 1) ) ; :: thesis: contradiction
hence contradiction by A2, A3, A10, A14, A11, Th4; :: thesis: verum
end;
case ( f . i = f . (j + 1) & f . (i + 1) = f . j ) ; :: thesis: contradiction
hence contradiction by A2, A3, A4, A12, A11, Th4; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence LSeg f,i misses LSeg f,j ; :: thesis: verum
end;
end;
end;
hence f is s.c.c. by GOBOARD5:def 4; :: thesis: verum
end;
suppose A23: len f < 1 ; :: thesis: f is s.c.c.
for i, j being Element of NAT st i + 1 < j & ( ( i > 1 & j < len f ) or j + 1 < len f ) holds
LSeg f,i misses LSeg f,j
proof
let i, j be Element of NAT ; :: thesis: ( i + 1 < j & ( ( i > 1 & j < len f ) or j + 1 < len f ) implies LSeg f,i misses LSeg f,j )
assume that
i + 1 < j and
( ( i > 1 & j < len f ) or j + 1 < len f ) ; :: thesis: LSeg f,i misses LSeg f,j
end;
hence f is s.c.c. by GOBOARD5:def 4; :: thesis: verum
end;
end;