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 Th7;
for i, j being 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 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 :: thesis: not LSeg (f,i) meets LSeg (f,j)
assume A17: LSeg (f,i) meets LSeg (f,j) ; :: thesis: contradiction
now :: thesis: ( ( (LSeg (f,i)) /\ (LSeg (f,j)) = {(f . i)} & ( f . i = f . j or f . i = f . (j + 1) ) & LSeg (f,i) <> LSeg (f,j) & contradiction ) 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) & contradiction ) or ( LSeg (f,i) = LSeg (f,j) & contradiction ) )
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;
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 :: thesis: ( ( f . i = f . j & contradiction ) or ( f . i = f . (j + 1) & contradiction ) )
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, Th1; :: thesis: verum
end;
case f . i = f . (j + 1) ; :: thesis: contradiction
hence contradiction by A2, A3, A5, A6, A15, A14, Th1; :: 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 :: thesis: ( ( f . (i + 1) = f . j & contradiction ) or ( f . (i + 1) = f . (j + 1) & contradiction ) )
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, Th1; :: thesis: verum
end;
case f . (i + 1) = f . (j + 1) ; :: thesis: contradiction
hence contradiction by A2, A3, A10, A14, A11, Th1; :: 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 3;
then A20: LSeg ((f /. i),(f /. (i + 1))) = LSeg ((f /. j),(f /. (j + 1))) by A8, A14, TOPREAL1:def 3;
A21: ( f /. j = f . j & f /. (j + 1) = f . (j + 1) ) by A8, A12, A14, A9, FINSEQ_4:15;
A22: ( f /. i = f . i & f /. (i + 1) = f . (i + 1) ) by A6, A13, A16, A11, FINSEQ_4:15;
now :: thesis: ( ( f . i = f . j & f . (i + 1) = f . (j + 1) & contradiction ) or ( f . i = f . (j + 1) & f . (i + 1) = f . j & contradiction ) )
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:8;
case ( f . i = f . j & f . (i + 1) = f . (j + 1) ) ; :: thesis: contradiction
hence contradiction by A2, A3, A10, A14, A11, Th1; :: thesis: verum
end;
case ( f . i = f . (j + 1) & f . (i + 1) = f . j ) ; :: thesis: contradiction
hence contradiction by A2, A3, A4, A12, A11, Th1; :: 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;
suppose i < 1 ; :: thesis: LSeg (f,i) misses LSeg (f,j)
then LSeg (f,i) = {} by TOPREAL1:def 3;
then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ;
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 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 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)
per cases ( i >= 1 or i < 1 ) ;
suppose i >= 1 ; :: thesis: LSeg (f,i) misses LSeg (f,j)
then i > len f by A23, XXREAL_0:2;
then i + 1 > len f by NAT_1:13;
then LSeg (f,i) = {} by TOPREAL1:def 3;
then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ;
hence LSeg (f,i) misses LSeg (f,j) ; :: thesis: verum
end;
suppose i < 1 ; :: thesis: LSeg (f,i) misses LSeg (f,j)
then LSeg (f,i) = {} by TOPREAL1:def 3;
then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ;
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;
end;