let G be _finite _Graph; 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; 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 S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A2:
S1[
k]
;
S1[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 A6:
k < G .order()
;
S1[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 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) . xlet x be
set ;
( not x in dom (((MCS:CSeq G) . (k + 1)) `1) implies card ((G .AdjacentSet {b1}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1))) = (((MCS:CSeq G) . (k + 1)) `2) . b1 )assume A14:
not
x in dom (((MCS:CSeq G) . (k + 1)) `1)
;
card ((G .AdjacentSet {b1}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1))) = (((MCS:CSeq G) . (k + 1)) `2) . b1A15:
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 A21:
( not
x in G .AdjacentSet {w} or
x in dom (((MCS:CSeq G) . k) `1) )
;
card ((G .AdjacentSet {b1}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1))) = (((MCS:CSeq G) . (k + 1)) `2) . b1set GAS =
G .AdjacentSet {x};
A22:
not
w in G .AdjacentSet {x}
by A13, A14, A21, CHORD:53, XBOOLE_0:def 3;
(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;
verum end; end; end; hence
S1[
k + 1]
;
verum end; end;
end;
then A27:
S1[ 0 ]
;
A28:
for k being Nat holds S1[k]
from NAT_1:sch 2(A27, A1);
let x be set ; ( 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)
; (((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; verum