let G be _finite _Graph; :: thesis: (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; :: according to LEXBFS:def 9 :: thesis: ( (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 :: thesis: 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; :: thesis: ( ((MCS:CSeq G) ``1) . k = ((MCS:CSeq G) ``1) . n implies ((MCS:CSeq G) ``1) . (b<sub>1</sub> + 1) = ((MCS:CSeq G) ``1) . (b₂ + 1) )
assume A2: ((MCS:CSeq G) ``1) . k = ((MCS:CSeq G) ``1) . n ; :: thesis: ((MCS:CSeq G) ``1) . (b<sub>1</sub> + 1) = ((MCS:CSeq G) ``1) . (b₂ + 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 A7: ( k <= G .order() & n <= G .order() ) ; :: thesis: ((MCS:CSeq G) ``1) . (b<sub>1</sub> + 1) = ((MCS:CSeq G) ``1) . (b₂ + 1)

then card (dom (((MCS:CSeq G) . n) `1)) = n by Th65;
hence ((MCS:CSeq G) ``1) . (k + 1) = ((MCS:CSeq G) ``1) . (n + 1) by A2, A4, A6, A7, Th65; :: thesis: verum

end;

suppose A8: ( k <= G .order() & n >= G .order() ) ; :: thesis: ((MCS:CSeq G) ``1) . (b<sub>1</sub> + 1) = ((MCS:CSeq G) ``1) . (b₂ + 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 ;
:: thesis: verum

end;

suppose A12: ( k >= G .order() & n <= G .order() ) ; :: thesis: ((MCS:CSeq G) ``1) . (b<sub>1</sub> + 1) = ((MCS:CSeq G) ``1) . (b₂ + 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 ;
:: thesis: verum

end;

suppose A16: ( k >= G .order() & n >= G .order() ) ; :: thesis: ((MCS:CSeq G) ``1) . (b<sub>1</sub> + 1) = ((MCS:CSeq G) ``1) . (b₂ + 1)

then A17: n + 1 >= G .order() by NAT_1:13;
A18: k + 1 >= G .order() by A16, NAT_1:13;
thus ((MCS:CSeq G) ``1) . (k + 1) = ((MCS:CSeq G) . (k + 1)) `1 by Def24
.= ((MCS:CSeq G) . (G .order())) `1 by A18, Th66
.= ((MCS:CSeq G) . (n + 1)) `1 by A17, Th66
.= ((MCS:CSeq G) ``1) . (n + 1) by Def24 ; :: thesis: verum

end;

end;

end;

hence (MCS:CSeq G) ``1 is iterative ; :: thesis: ( (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 ; :: thesis: ( ((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; :: thesis: 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; :: thesis: ( 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() ; :: thesis: 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); :: thesis: ( 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; :: thesis: ((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; :: thesis: verum