let G be _finite _Graph; :: thesis: for n being Nat
for x being set st not x in dom (((MCS:CSeq G) . n) `1) holds
(((MCS:CSeq G) . n) `2) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . n) `1)))
let n be Nat; :: thesis: for x being set st not x in dom (((MCS:CSeq G) . n) `1) holds
(((MCS:CSeq G) . n) `2) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . n) `1)))
set CN = (MCS:CSeq G) . n;
set VLN = ((MCS:CSeq G) . n) `1 ;
defpred S<sub>1</sub>[ Nat] means for x being set st not x in dom (((MCS:CSeq G) . $1) `1) holds
(((MCS:CSeq G) . $1) `2) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . $1) `1)));
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
set CS1 = (MCS:CSeq G) . (k + 1);
set CSK = (MCS:CSeq G) . k;
set VLK = ((MCS:CSeq G) . k) `1 ;
set VK2 = ((MCS:CSeq G) . k) `2 ;
set VL1 = ((MCS:CSeq G) . (k + 1)) `1 ;
set V12 = ((MCS:CSeq G) . (k + 1)) `2 ;
A3: k <= k + 1 by XREAL_1:38;

per cases ( G .order() <= k or k < G .order() ) ;

suppose A4: G .order() <= k ; :: thesis: S₁[k + 1]

then A5: ((MCS:CSeq G) . k) `2 = ((MCS:CSeq G) . (k + 1)) `2 by A3, Th67;
((MCS:CSeq G) . k) `1 = ((MCS:CSeq G) . (k + 1)) `1 by A3, A4, Th67;
hence S₁[k + 1] by A2, A5; :: thesis: verum

end;

suppose A6: k < G .order() ; :: thesis: S₁[k + 1]

set VL = (MCS:CSeq G) ``1 ;
A7: G .order() = (MCS:CSeq G) .Lifespan() by Th70;
A8: ((MCS:CSeq G) . k) `1 = ((MCS:CSeq G) ``1) . k by Def24;
A9: (MCS:CSeq G) .Lifespan() = ((MCS:CSeq G) ``1) .Lifespan() by Th72;
A10: ((MCS:CSeq G) . (k + 1)) `1 = ((MCS:CSeq G) ``1) . (k + 1) by Def24;
consider w being Vertex of G such that
A11: w = MCS:PickUnnumbered ((MCS:CSeq G) . k) and
A12: for v being set holds
( ( v in G .AdjacentSet {w} & not v in dom (((MCS:CSeq G) . k) `1) implies (((MCS:CSeq G) . (k + 1)) `2) . v = ((((MCS:CSeq G) . k) `2) . v) + 1 ) & ( ( not v in G .AdjacentSet {w} or v in dom (((MCS:CSeq G) . k) `1) ) implies (((MCS:CSeq G) . (k + 1)) `2) . v = (((MCS:CSeq G) . k) `2) . v ) ) by A6, Th75;
w = ((MCS:CSeq G) ``1) .PickedAt k by A6, A11, Th74;
then A13: dom (((MCS:CSeq G) . (k + 1)) `1) = (dom (((MCS:CSeq G) . k) `1)) \/ {w} by A6, A7, A8, A10, A9, Th11;

now :: thesis: for x being set st not x in dom (((MCS:CSeq G) . (k + 1)) `1) holds
card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1))) = (((MCS:CSeq G) . (k + 1)) `2) . x

let x be set ; :: thesis: ( not x in dom (((MCS:CSeq G) . (k + 1)) `1) implies card ((G .AdjacentSet {b<sub>1</sub>}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1))) = (((MCS:CSeq G) . (k + 1)) `2) . b<sub>1</sub> )
assume A14: not x in dom (((MCS:CSeq G) . (k + 1)) `1) ; :: thesis: card ((G .AdjacentSet {b₁}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1))) = (((MCS:CSeq G) . (k + 1)) `2) . b₁
A15: not x in dom (((MCS:CSeq G) . k) `1) by A13, A14, XBOOLE_0:def 3;
then A16: card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1))) = (((MCS:CSeq G) . k) `2) . x by A2;

per cases ( ( x in G .AdjacentSet {w} & not x in dom (((MCS:CSeq G) . k) `1) ) or not x in G .AdjacentSet {w} or x in dom (((MCS:CSeq G) . k) `1) ) ;

suppose A17: ( x in G .AdjacentSet {w} & not x in dom (((MCS:CSeq G) . k) `1) ) ; :: thesis: card ((G .AdjacentSet {b<sub>1</sub>}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1))) = (((MCS:CSeq G) . (k + 1)) `2) . b₁

set GAS = G .AdjacentSet {x};
w in G .AdjacentSet {x} by A17, CHORD:53;
then A18: {w} c= G .AdjacentSet {x} by ZFMISC_1:31;
A19: (G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1)) = ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1))) \/ ((G .AdjacentSet {x}) /\ {w}) by A13, XBOOLE_1:23
.= ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1))) \/ {w} by A18, XBOOLE_1:28 ;
dom (((MCS:CSeq G) . k) `1) <> the_Vertices_of G by A6, Th69;
then not w in dom (((MCS:CSeq G) . k) `1) by A11, Th59;
then A20: not w in (G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1)) by XBOOLE_0:def 4;
(((MCS:CSeq G) . (k + 1)) `2) . x = ((((MCS:CSeq G) . k) `2) . x) + 1 by A12, A17;
hence card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1))) = (((MCS:CSeq G) . (k + 1)) `2) . x by A16, A20, A19, CARD_2:41; :: thesis: verum

end;

suppose A21: ( not x in G .AdjacentSet {w} or x in dom (((MCS:CSeq G) . k) `1) ) ; :: thesis: card ((G .AdjacentSet {b<sub>1</sub>}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1))) = (((MCS:CSeq G) . (k + 1)) `2) . b₁

set GAS = G .AdjacentSet {x};
A22: not w in G .AdjacentSet {x} by A13, A14, A21, CHORD:53, XBOOLE_0:def 3;

A23: now :: thesis: not (G .AdjacentSet {x}) /\ {w} = {w}

assume (G .AdjacentSet {x}) /\ {w} = {w} ; :: thesis: contradiction
then w in (G .AdjacentSet {x}) /\ {w} by TARSKI:def 1;
hence contradiction by A22, XBOOLE_0:def 4; :: thesis: verum

end;

(G .AdjacentSet {x}) /\ {w} c= {w} by XBOOLE_1:17;
then (G .AdjacentSet {x}) /\ {w} in bool {w} ;
then A24: (G .AdjacentSet {x}) /\ {w} in {{},{w}} by ZFMISC_1:24;
A25: (((MCS:CSeq G) . (k + 1)) `2) . x = (((MCS:CSeq G) . k) `2) . x by A12, A21;
(G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1)) = ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1))) \/ ((G .AdjacentSet {x}) /\ {w}) by A13, XBOOLE_1:23
.= ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1))) \/ {} by A24, A23, TARSKI:def 2
.= (G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1)) ;
hence card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1))) = (((MCS:CSeq G) . (k + 1)) `2) . x by A2, A15, A25; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

end;

end;

now :: thesis: for x being set st not x in dom (((MCS:CSeq G) . 0) `1) holds
(((MCS:CSeq G) . 0) `2) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . 0) `1)))

set C0 = (MCS:CSeq G) . 0;
let x be set ; :: thesis: ( not x in dom (((MCS:CSeq G) . 0) `1) implies (((MCS:CSeq G) . 0) `2) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . 0) `1))) )
set VL0 = ((MCS:CSeq G) . 0) `1 ;
set V20 = ((MCS:CSeq G) . 0) `2 ;
assume not x in dom (((MCS:CSeq G) . 0) `1) ; :: thesis: (((MCS:CSeq G) . 0) `2) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . 0) `1)))
A26: (MCS:CSeq G) . 0 = MCS:Init G by Def25;
dom (((MCS:CSeq G) . 0) `1) = {} by A26;
hence (((MCS:CSeq G) . 0) `2) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . 0) `1))) by A26; :: thesis: verum

end;

then A27: S₁[ 0 ] ;
A28: for k being Nat holds S₁[k] from NAT_1:sch 2(A27, A1);
let x be set ; :: thesis: ( not x in dom (((MCS:CSeq G) . n) `1) implies (((MCS:CSeq G) . n) `2) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . n) `1))) )
assume not x in dom (((MCS:CSeq G) . n) `1) ; :: thesis: (((MCS:CSeq G) . n) `2) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . n) `1)))
hence (((MCS:CSeq G) . n) `2) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . n) `1))) by A28; :: thesis: verum