let G be _finite _Graph; (MCS:CSeq G) ``1 is vertex-numbering
set GS = MCS:CSeq G;
set S = (MCS:CSeq G) ``1 ;
A1:
(MCS:CSeq G) . 0 = MCS:Init G
by Def25;
((MCS:CSeq G) ``1) . 0 = ((MCS:CSeq G) . 0) `1
by Def24;
hence
((MCS:CSeq G) ``1) . 0 = {}
by A1; LEXBFS:def 9 ( (MCS:CSeq G) ``1 is iterative & (MCS:CSeq G) ``1 is halting & ((MCS:CSeq G) ``1) .Lifespan() = G .order() & ( for n being Nat st n < ((MCS:CSeq G) ``1) .Lifespan() holds
ex w being Vertex of G st
( not w in dom (((MCS:CSeq G) ``1) . n) & ((MCS:CSeq G) ``1) . (n + 1) = (((MCS:CSeq G) ``1) . n) +* (w .--> ((((MCS:CSeq G) ``1) .Lifespan()) -' n)) ) ) )
now for k, n being Nat st ((MCS:CSeq G) ``1) . k = ((MCS:CSeq G) ``1) . n holds
((MCS:CSeq G) ``1) . (k + 1) = ((MCS:CSeq G) ``1) . (n + 1)let k,
n be
Nat;
( ((MCS:CSeq G) ``1) . k = ((MCS:CSeq G) ``1) . n implies ((MCS:CSeq G) ``1) . (b1 + 1) = ((MCS:CSeq G) ``1) . (b2 + 1) )assume A2:
((MCS:CSeq G) ``1) . k = ((MCS:CSeq G) ``1) . n
;
((MCS:CSeq G) ``1) . (b1 + 1) = ((MCS:CSeq G) ``1) . (b2 + 1)A3:
((MCS:CSeq G) ``1) . (k + 1) = ((MCS:CSeq G) . (k + 1)) `1
by Def24;
A4:
((MCS:CSeq G) ``1) . k = ((MCS:CSeq G) . k) `1
by Def24;
A5:
((MCS:CSeq G) ``1) . (n + 1) = ((MCS:CSeq G) . (n + 1)) `1
by Def24;
A6:
((MCS:CSeq G) ``1) . n = ((MCS:CSeq G) . n) `1
by Def24;
per cases
( ( k <= G .order() & n <= G .order() ) or ( k <= G .order() & n >= G .order() ) or ( k >= G .order() & n <= G .order() ) or ( k >= G .order() & n >= G .order() ) )
;
suppose A8:
(
k <= G .order() &
n >= G .order() )
;
((MCS:CSeq G) ``1) . (b1 + 1) = ((MCS:CSeq G) ``1) . (b2 + 1)then A9:
(MCS:CSeq G) . n = (MCS:CSeq G) . (G .order())
by Th66;
A10:
card (dom (((MCS:CSeq G) . (G .order())) `1)) = G .order()
by Th65;
A11:
n + 1
>= G .order()
by A8, NAT_1:13;
card (dom (((MCS:CSeq G) . k) `1)) = k
by A8, Th65;
then
k + 1
>= G .order()
by A2, A4, A6, A9, A10, NAT_1:13;
hence ((MCS:CSeq G) ``1) . (k + 1) =
((MCS:CSeq G) . (G .order())) `1
by A3, Th66
.=
((MCS:CSeq G) ``1) . (n + 1)
by A5, A11, Th66
;
verum end; suppose A12:
(
k >= G .order() &
n <= G .order() )
;
((MCS:CSeq G) ``1) . (b1 + 1) = ((MCS:CSeq G) ``1) . (b2 + 1)then A13:
(MCS:CSeq G) . k = (MCS:CSeq G) . (G .order())
by Th66;
A14:
card (dom (((MCS:CSeq G) . (G .order())) `1)) = G .order()
by Th65;
card (dom (((MCS:CSeq G) . n) `1)) = n
by A12, Th65;
then A15:
n + 1
>= G .order()
by A2, A4, A6, A13, A14, NAT_1:13;
k + 1
>= G .order()
by A12, NAT_1:13;
hence ((MCS:CSeq G) ``1) . (k + 1) =
((MCS:CSeq G) . (G .order())) `1
by A3, Th66
.=
((MCS:CSeq G) ``1) . (n + 1)
by A5, A15, Th66
;
verum end; end; end;
hence
(MCS:CSeq G) ``1 is iterative
; ( (MCS:CSeq G) ``1 is halting & ((MCS:CSeq G) ``1) .Lifespan() = G .order() & ( for n being Nat st n < ((MCS:CSeq G) ``1) .Lifespan() holds
ex w being Vertex of G st
( not w in dom (((MCS:CSeq G) ``1) . n) & ((MCS:CSeq G) ``1) . (n + 1) = (((MCS:CSeq G) ``1) . n) +* (w .--> ((((MCS:CSeq G) ``1) .Lifespan()) -' n)) ) ) )
(MCS:CSeq G) ``1 is eventually-constant
by Th71;
hence
(MCS:CSeq G) ``1 is halting
; ( ((MCS:CSeq G) ``1) .Lifespan() = G .order() & ( for n being Nat st n < ((MCS:CSeq G) ``1) .Lifespan() holds
ex w being Vertex of G st
( not w in dom (((MCS:CSeq G) ``1) . n) & ((MCS:CSeq G) ``1) . (n + 1) = (((MCS:CSeq G) ``1) . n) +* (w .--> ((((MCS:CSeq G) ``1) .Lifespan()) -' n)) ) ) )
(MCS:CSeq G) .Lifespan() = ((MCS:CSeq G) ``1) .Lifespan()
by Th72;
hence A19:
((MCS:CSeq G) ``1) .Lifespan() = G .order()
by Th70; for n being Nat st n < ((MCS:CSeq G) ``1) .Lifespan() holds
ex w being Vertex of G st
( not w in dom (((MCS:CSeq G) ``1) . n) & ((MCS:CSeq G) ``1) . (n + 1) = (((MCS:CSeq G) ``1) . n) +* (w .--> ((((MCS:CSeq G) ``1) .Lifespan()) -' n)) )
let n be Nat; ( n < ((MCS:CSeq G) ``1) .Lifespan() implies ex w being Vertex of G st
( not w in dom (((MCS:CSeq G) ``1) . n) & ((MCS:CSeq G) ``1) . (n + 1) = (((MCS:CSeq G) ``1) . n) +* (w .--> ((((MCS:CSeq G) ``1) .Lifespan()) -' n)) ) )
assume A20:
n < ((MCS:CSeq G) ``1) .Lifespan()
; ex w being Vertex of G st
( not w in dom (((MCS:CSeq G) ``1) . n) & ((MCS:CSeq G) ``1) . (n + 1) = (((MCS:CSeq G) ``1) . n) +* (w .--> ((((MCS:CSeq G) ``1) .Lifespan()) -' n)) )
take w = MCS:PickUnnumbered ((MCS:CSeq G) . n); ( not w in dom (((MCS:CSeq G) ``1) . n) & ((MCS:CSeq G) ``1) . (n + 1) = (((MCS:CSeq G) ``1) . n) +* (w .--> ((((MCS:CSeq G) ``1) .Lifespan()) -' n)) )
A21:
((MCS:CSeq G) . n) `1 = ((MCS:CSeq G) ``1) . n
by Def24;
then
dom (((MCS:CSeq G) ``1) . n) <> the_Vertices_of G
by A19, A20, Th69;
hence
not w in dom (((MCS:CSeq G) ``1) . n)
by A21, Th59; ((MCS:CSeq G) ``1) . (n + 1) = (((MCS:CSeq G) ``1) . n) +* (w .--> ((((MCS:CSeq G) ``1) .Lifespan()) -' n))
A22:
((MCS:CSeq G) . (n + 1)) `1 = ((MCS:CSeq G) ``1) . (n + 1)
by Def24;
n = card (dom (((MCS:CSeq G) ``1) . n))
by A19, A20, A21, Th65;
hence
((MCS:CSeq G) ``1) . (n + 1) = (((MCS:CSeq G) ``1) . n) +* (w .--> ((((MCS:CSeq G) ``1) .Lifespan()) -' n))
by A19, A20, A21, A22, Th64; verum