let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is nodic & PairF f is Simple implies f is s.c.c. )
assume A1: ( f is nodic & 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 A2: 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 A3: ( i + 1 < j & ( ( 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 A4: i >= 1 ; :: thesis: LSeg f,i misses LSeg f,j
A5: i < j by A3, NAT_1:13;
A6: i + 1 < j + 1 by A3, NAT_1:13;
A7: 1 <= j by A4, A5, XXREAL_0:2;
A8: j < len f by A3, NAT_1:13;
then A9: i + 1 < len f by A3, XXREAL_0:2;
A10: i < j + 1 by A5, NAT_1:13;
A11: j + 1 <= len f by A3, NAT_1:13;
then A12: i < len f by A10, XXREAL_0:2;
A13: 1 < i + 1 by A4, NAT_1:13;
A14: 1 < j + 1 by A7, NAT_1:13;
now
assume A15: 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, A15, Def4;
case A16: ( (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 A16;
case f . i = f . j ; :: thesis: contradiction
hence contradiction by A1, A2, A4, A5, A8, Th4; :: thesis: verum
end;
case f . i = f . (j + 1) ; :: thesis: contradiction
hence contradiction by A1, A2, A3, A4, A10, A11, Th4; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
case A17: ( (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 A17;
case f . (i + 1) = f . j ; :: thesis: contradiction
hence contradiction by A1, A2, A3, A8, A13, Th4; :: thesis: verum
end;
case f . (i + 1) = f . (j + 1) ; :: thesis: contradiction
hence contradiction by A1, A2, A6, A11, A13, 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 A4, A9, TOPREAL1:def 5;
then A18: LSeg (f /. i),(f /. (i + 1)) = LSeg (f /. j),(f /. (j + 1)) by A7, A11, TOPREAL1:def 5;
A19: f /. i = f . i by A4, A12, FINSEQ_4:24;
A20: f /. (i + 1) = f . (i + 1) by A9, A13, FINSEQ_4:24;
A21: f /. j = f . j by A7, A8, FINSEQ_4:24;
A22: f /. (j + 1) = f . (j + 1) by A11, A14, 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 A18, A19, A20, A21, A22, SPPOL_1:25;
case ( f . i = f . j & f . (i + 1) = f . (j + 1) ) ; :: thesis: contradiction
hence contradiction by A1, A2, A6, A11, A13, Th4; :: thesis: verum
end;
case ( f . i = f . (j + 1) & f . (i + 1) = f . j ) ; :: thesis: contradiction
hence contradiction by A1, A2, A3, A8, A13, 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 ( i + 1 < j & ( ( 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;