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 Def26;
A2: [{},((the_Vertices_of G) --> 0)] `1 = {} ;
((MCS:CSeq G) ``1) . 0 = ((MCS:CSeq G) . 0) `1 by Def25;
hence ((MCS:CSeq G) ``1) . 0 = {} by A1, A2; :: 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 A3: ((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)
A4: ((MCS:CSeq G) ``1) . (k + 1) = ((MCS:CSeq G) . (k + 1)) `1 by Def25;
A5: ((MCS:CSeq G) ``1) . k = ((MCS:CSeq G) . k) `1 by Def25;
A6: ((MCS:CSeq G) ``1) . (n + 1) = ((MCS:CSeq G) . (n + 1)) `1 by Def25;
A7: ((MCS:CSeq G) ``1) . n = ((MCS:CSeq G) . n) `1 by Def25;

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() ) ; :: 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 A3, A5, A7, A8, Th65; :: thesis: verum

end;

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

then A10: (MCS:CSeq G) . n = (MCS:CSeq G) . (G .order()) by Th66;
A11: card (dom (((MCS:CSeq G) . (G .order())) `1)) = G .order() by Th65;
A12: n + 1 >= G .order() by A9, NAT_1:13;
card (dom (((MCS:CSeq G) . k) `1)) = k by A9, Th65;
then k + 1 >= G .order() by A3, A5, A7, A10, A11, NAT_1:13;
hence ((MCS:CSeq G) ``1) . (k + 1) = ((MCS:CSeq G) . (G .order())) `1 by A4, Th66
.= ((MCS:CSeq G) ``1) . (n + 1) by A6, A12, Th66 ;
:: thesis: verum

end;

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

then A14: (MCS:CSeq G) . k = (MCS:CSeq G) . (G .order()) by Th66;
A15: card (dom (((MCS:CSeq G) . (G .order())) `1)) = G .order() by Th65;
card (dom (((MCS:CSeq G) . n) `1)) = n by A13, Th65;
then A16: n + 1 >= G .order() by A3, A5, A7, A14, A15, NAT_1:13;
k + 1 >= G .order() by A13, NAT_1:13;
hence ((MCS:CSeq G) ``1) . (k + 1) = ((MCS:CSeq G) . (G .order())) `1 by A4, Th66
.= ((MCS:CSeq G) ``1) . (n + 1) by A6, A16, Th66 ;
:: thesis: verum

end;

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

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

end;

end;

end;

hence (MCS:CSeq G) ``1 is iterative by Def6; :: 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 A20: ((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 A21: 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)) )
A22: ((MCS:CSeq G) . n) `1 = ((MCS:CSeq G) ``1) . n by Def25;
then dom (((MCS:CSeq G) ``1) . n) <> the_Vertices_of G by A20, A21, Th69;
hence not w in dom (((MCS:CSeq G) ``1) . n) by A22, Th59; :: thesis: ((MCS:CSeq G) ``1) . (n + 1) = (((MCS:CSeq G) ``1) . n) +* (w .--> ((((MCS:CSeq G) ``1) .Lifespan()) -' n))
A23: ((MCS:CSeq G) . (n + 1)) `1 = ((MCS:CSeq G) ``1) . (n + 1) by Def25;
n = card (dom (((MCS:CSeq G) ``1) . n)) by A20, A21, A22, Th65;
hence ((MCS:CSeq G) ``1) . (n + 1) = (((MCS:CSeq G) ``1) . n) +* (w .--> ((((MCS:CSeq G) ``1) .Lifespan()) -' n)) by A20, A21, A22, A23, Th64; :: thesis: verum