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:40;

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 Def25;
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 Def25;
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

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:37;
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:54; :: 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

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:30;
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

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 Def26;
then dom (((MCS:CSeq G) . 0 ) `1 ) = {} by MCART_1:def 1, RELAT_1:60;
hence (((MCS:CSeq G) . 0 ) `2 ) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . 0 ) `1 ))) by A26, Th57, CARD_1:47; :: 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
set VL2 = ((MCS:CSeq G) . n) `2 ;