let G be finite _Graph; :: thesis: (MCS:CSeq G) ``1 is vertex-numbering
set GS = MCS:CSeq G;
set S = (MCS:CSeq G) ``1 ;
Aa: ((MCS:CSeq G) ``1 ) . 0 = ((MCS:CSeq G) . 0 ) `1 by d1stMCSLS;
(MCS:CSeq G) . 0 = MCS:Init G by Def40;
hence ((MCS:CSeq G) ``1 ) . 0 = {} by MCART_1:def 1, Aa; :: 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

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 A: ((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)
B: ((MCS:CSeq G) ``1 ) . k = ((MCS:CSeq G) . k) `1 by d1stMCSLS;
C: ((MCS:CSeq G) ``1 ) . n = ((MCS:CSeq G) . n) `1 by d1stMCSLS;
B1: ((MCS:CSeq G) ``1 ) . (k + 1) = ((MCS:CSeq G) . (k + 1)) `1 by d1stMCSLS;
C1: ((MCS:CSeq G) ``1 ) . (n + 1) = ((MCS:CSeq G) . (n + 1)) `1 by d1stMCSLS;

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

card (dom (((MCS:CSeq G) . n) `1 )) = n by S1, Th82;
hence ((MCS:CSeq G) ``1 ) . (k + 1) = ((MCS:CSeq G) ``1 ) . (n + 1) by A, B, C, S1, Th82; :: thesis: verum

end;

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

A1: card (dom (((MCS:CSeq G) . k) `1 )) = k by S1, Th82;
A2: (MCS:CSeq G) . n = (MCS:CSeq G) . (G .order() ) by S1, Th83;
A3: card (dom (((MCS:CSeq G) . (G .order() )) `1 )) = G .order() by Th82;
A5: k + 1 >= G .order() by NAT_1:13, A, B, C, A1, A2, A3;
A6: n + 1 >= G .order() by S1, NAT_1:13;
thus ((MCS:CSeq G) ``1 ) . (k + 1) = ((MCS:CSeq G) . (G .order() )) `1 by B1, A5, Th83
.= ((MCS:CSeq G) ``1 ) . (n + 1) by C1, A6, Th83 ; :: thesis: verum

end;

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

A1: card (dom (((MCS:CSeq G) . n) `1 )) = n by S1, Th82;
A2: (MCS:CSeq G) . k = (MCS:CSeq G) . (G .order() ) by S1, Th83;
A3: card (dom (((MCS:CSeq G) . (G .order() )) `1 )) = G .order() by Th82;
A5: n + 1 >= G .order() by NAT_1:13, A, B, C, A1, A2, A3;
A6: k + 1 >= G .order() by S1, NAT_1:13;
thus ((MCS:CSeq G) ``1 ) . (k + 1) = ((MCS:CSeq G) . (G .order() )) `1 by B1, A6, Th83
.= ((MCS:CSeq G) ``1 ) . (n + 1) by C1, A5, Th83 ; :: thesis: verum

end;

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

then A1: ( k + 1 >= G .order() & n + 1 >= G .order() ) by NAT_1:13;
thus ((MCS:CSeq G) ``1 ) . (k + 1) = ((MCS:CSeq G) . (k + 1)) `1 by d1stMCSLS
.= ((MCS:CSeq G) . (G .order() )) `1 by A1, Th83
.= ((MCS:CSeq G) . (n + 1)) `1 by A1, Th83
.= ((MCS:CSeq G) ``1 ) . (n + 1) by d1stMCSLS ; :: thesis: verum

end;

end;

end;

hence (MCS:CSeq G) ``1 is iterative by Def15; :: 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 mVNS0a;
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 mVNS0;
hence A3: ((MCS:CSeq G) ``1 ) .Lifespan() = G .order() by Th87; :: 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 A4: 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)) )
Aa: ((MCS:CSeq G) . n) `1 = ((MCS:CSeq G) ``1 ) . n by d1stMCSLS;
Ab: ((MCS:CSeq G) . (n + 1)) `1 = ((MCS:CSeq G) ``1 ) . (n + 1) by d1stMCSLS;
dom (((MCS:CSeq G) ``1 ) . n) <> the_Vertices_of G by Aa, A3, A4, Th86;
hence not w in dom (((MCS:CSeq G) ``1 ) . n) by Aa, Th73; :: thesis: ((MCS:CSeq G) ``1 ) . (n + 1) = (((MCS:CSeq G) ``1 ) . n) +* (w .--> ((((MCS:CSeq G) ``1 ) .Lifespan() ) -' n))
n = card (dom (((MCS:CSeq G) ``1 ) . n)) by Aa, A3, A4, Th82;
hence ((MCS:CSeq G) ``1 ) . (n + 1) = (((MCS:CSeq G) ``1 ) . n) +* (w .--> ((((MCS:CSeq G) ``1 ) .Lifespan() ) -' n)) by Aa, Ab, A3, A4, Th81; :: thesis: verum