let G be finite SimpleGraph; :: thesis: for n being Nat holds size ((MycielskianSeq G) . n) = (((3 |^ n) * (size G)) + (((3 |^ n) - (2 |^ n)) * (order G))) + ((n + 1) block 3)
let n be Nat; :: thesis: size ((MycielskianSeq G) . n) = (((3 |^ n) * (size G)) + (((3 |^ n) - (2 |^ n)) * (order G))) + ((n + 1) block 3)
set g = order G;
set s = size G;
set MG = MycielskianSeq G;
defpred S₁[ Nat] means size ((MycielskianSeq G) . $1) = (((3 |^ $1) * (size G)) + (((3 |^ $1) - (2 |^ $1)) * (order G))) + (($1 + 1) block 3);
A1: S₁[ 0 ]

proof

thus size ((MycielskianSeq G) . 0) = ((1 * (size G)) + (0 * (order G))) + 0 by Th113
.= (((3 |^ 0) * (size G)) + ((1 - 1) * (order G))) + 0 by NEWTON:4
.= (((3 |^ 0) * (size G)) + (((3 |^ 0) - 1) * (order G))) + 0 by NEWTON:4
.= (((3 |^ 0) * (size G)) + (((3 |^ 0) - (2 |^ 0)) * (order G))) + 0 by NEWTON:4
.= (((3 |^ 0) * (size G)) + (((3 |^ 0) - (2 |^ 0)) * (order G))) + ((0 + 1) block 3) by STIRL2_1:29 ; :: thesis: verum

end;

A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
A4: n + 1 >= 0 + 1 by XREAL_1:6;
A5: (1 / 2) * ((2 |^ (n + 1)) - 2) = (1 / 2) * ((2 * (2 |^ n)) - (2 * 1)) by NEWTON:6
.= (2 |^ n) - 1 ;
thus size ((MycielskianSeq G) . (n + 1)) = size (Mycielskian ((MycielskianSeq G) . n)) by Th115
.= (3 * ((((3 |^ n) * (size G)) + (((3 |^ n) - (2 |^ n)) * (order G))) + ((n + 1) block 3))) + (order ((MycielskianSeq G) . n)) by A3, Th92
.= ((((3 * (3 |^ n)) * (size G)) + ((3 * ((3 |^ n) - (2 |^ n))) * (order G))) + (3 * ((n + 1) block 3))) + (order ((MycielskianSeq G) . n))
.= ((((3 |^ (n + 1)) * (size G)) + ((3 * ((3 |^ n) - (2 |^ n))) * (order G))) + (3 * ((n + 1) block 3))) + (order ((MycielskianSeq G) . n)) by NEWTON:6
.= ((((3 |^ (n + 1)) * (size G)) + ((3 * ((3 |^ n) - (2 |^ n))) * (order G))) + (3 * ((n + 1) block 3))) + ((((2 |^ n) * (order G)) + (2 |^ n)) - 1) by Th116
.= ((((3 |^ (n + 1)) * (size G)) + ((3 * ((3 |^ n) - (2 |^ n))) * (order G))) + ((2 |^ n) * (order G))) + ((3 * ((n + 1) block 3)) + ((2 |^ n) - 1))
.= ((((3 |^ (n + 1)) * (size G)) + ((3 * ((3 |^ n) - (2 |^ n))) * (order G))) + ((2 |^ n) * (order G))) + (((2 + 1) * ((n + 1) block (2 + 1))) + ((n + 1) block 2)) by A5, A4, STIRL2_1:47
.= (((3 |^ (n + 1)) * (size G)) + ((((3 * (3 |^ n)) * (order G)) - (((2 * (2 |^ n)) * (order G)) + ((2 |^ n) * (order G)))) + ((2 |^ n) * (order G)))) + (((n + 1) + 1) block 3) by STIRL2_1:46
.= (((3 |^ (n + 1)) * (size G)) + ((((3 * (3 |^ n)) * (order G)) - (((2 |^ (n + 1)) * (order G)) + ((2 |^ n) * (order G)))) + ((2 |^ n) * (order G)))) + (((n + 1) + 1) block 3) by NEWTON:6
.= (((3 |^ (n + 1)) * (size G)) + (((((3 * (3 |^ n)) * (order G)) - ((2 |^ (n + 1)) * (order G))) - ((2 |^ n) * (order G))) + ((2 |^ n) * (order G)))) + (((n + 1) + 1) block 3)
.= (((3 |^ (n + 1)) * (size G)) + (((((3 |^ (n + 1)) * (order G)) - ((2 |^ (n + 1)) * (order G))) - ((2 |^ n) * (order G))) + ((2 |^ n) * (order G)))) + (((n + 1) + 1) block 3) by NEWTON:6
.= (((3 |^ (n + 1)) * (size G)) + (((3 |^ (n + 1)) - (2 |^ (n + 1))) * (order G))) + (((n + 1) + 1) block 3) ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence size ((MycielskianSeq G) . n) = (((3 |^ n) * (size G)) + (((3 |^ n) - (2 |^ n)) * (order G))) + ((n + 1) block 3) ; :: thesis: verum