let p, q be XFinSequence of ; :: thesis: for k being Element of NAT st p | ((2 * k) + (len q)) = ((k --> 0 ) ^ q) ^ (k --> 1) & q is dominated_by_0 & 2 * (Sum q) = len q & k > 0 holds
min* { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } = (2 * k) + (len q)
let k be Element of NAT ; :: thesis: ( p | ((2 * k) + (len q)) = ((k --> 0 ) ^ q) ^ (k --> 1) & q is dominated_by_0 & 2 * (Sum q) = len q & k > 0 implies min* { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } = (2 * k) + (len q) )
assume that
A1: p | ((2 * k) + (len q)) = ((k --> 0 ) ^ q) ^ (k --> 1) and
A2: ( q is dominated_by_0 & 2 * (Sum q) = len q ) and
A3: k > 0 ; :: thesis: min* { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } = (2 * k) + (len q)
set M = { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } ;
A4: { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } c= NAT

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } or y in NAT )
assume A5: y in { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } ; :: thesis: y in NAT
ex i being Element of NAT st
( i = y & 2 * (Sum (p | i)) = i & i > 0 ) by A5;
hence y in NAT ; :: thesis: verum

end;

set k0 = k --> 0 ;
set k1 = k --> 1;
set kqk = ((k --> 0 ) ^ q) ^ (k --> 1);
Sum (((k --> 0 ) ^ q) ^ (k --> 1)) = (Sum ((k --> 0 ) ^ q)) + (Sum (k --> 1)) by Lm4;
then ( Sum (((k --> 0 ) ^ q) ^ (k --> 1)) = ((Sum (k --> 0 )) + (Sum q)) + (Sum (k --> 1)) & Sum (k --> 0 ) = k * 0 & Sum (k --> 1) = k * 1 ) by Lm2, Lm4;
then ( 2 * (Sum (((k --> 0 ) ^ q) ^ (k --> 1))) = (len q) + (2 * k) & len q >= 0 & 2 * k > 0 ) by A2, A3, XREAL_1:70;
then ( 2 * (Sum (p | ((2 * k) + (len q)))) = (len q) + (2 * k) & (len q) + (2 * k) > 0 + 0 ) by A1;
then A6: (2 * k) + (len q) in { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } ;
then reconsider M = { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } as non empty Subset of NAT by A4;
min* M = (2 * k) + (len q)

proof

assume A7: min* M <> (2 * k) + (len q) ; :: thesis: contradiction
((k --> 0 ) ^ q) ^ (k --> 1) = (k --> 0 ) ^ (q ^ (k --> 1)) by AFINSQ_1:30;
then ( len (((k --> 0 ) ^ q) ^ (k --> 1)) = (len (k --> 0 )) + (len (q ^ (k --> 1))) & len (k --> 0 ) = dom (k --> 0 ) & dom (k --> 0 ) = k ) by AFINSQ_1:20, FUNCOP_1:19;
then A8: ( len (((k --> 0 ) ^ q) ^ (k --> 1)) = k + ((len q) + (len (k --> 1))) & len (k --> 1) = dom (k --> 1) & dom (k --> 1) = k & (2 * k) + (len q) >= min* M ) by A6, AFINSQ_1:20, FUNCOP_1:19, NAT_1:def 1;
then A9: min* M c= (2 * k) + (len q) by NAT_1:40;
then A10: p | (min* M) = (((k --> 0 ) ^ q) ^ (k --> 1)) | (min* M) by A1, RELAT_1:103;
min* M in M by NAT_1:def 1;
then A11: ex i being Element of NAT st
( i = min* M & 2 * (Sum (p | i)) = i & i > 0 ) ;

now

per cases ( min* M <= k or min* M > k ) ;

suppose A12: min* M <= k ; :: thesis: contradiction

( k = dom (k --> 0 ) & ((k --> 0 ) ^ q) ^ (k --> 1) = (k --> 0 ) ^ (q ^ (k --> 1)) ) by AFINSQ_1:30, FUNCOP_1:19;
then ( (((k --> 0 ) ^ q) ^ (k --> 1)) | (min* M) = (k --> 0 ) | (min* M) & (k --> 0 ) | (min* M) = (min* M) --> 0 ) by A12, Lm1, Th2;
then ( Sum (p | (min* M)) = Sum ((min* M) --> 0 ) & Sum ((min* M) --> 0 ) = (min* M) * 0 ) by A1, A9, Lm2, RELAT_1:103;
hence contradiction by A11; :: thesis: verum

end;

suppose min* M > k ; :: thesis: contradiction

then reconsider mk = (min* M) - k as Element of NAT by NAT_1:21;

now

per cases ( min* M <= k + (len q) or min* M > k + (len q) ) ;

suppose A13: min* M <= k + (len q) ; :: thesis: contradiction

( dom ((k --> 0 ) ^ q) = (len (k --> 0 )) + (len q) & len (k --> 0 ) = dom (k --> 0 ) & dom (k --> 0 ) = k & min* M = mk + k ) by AFINSQ_1:def 4, FUNCOP_1:19;
then ( (((k --> 0 ) ^ q) ^ (k --> 1)) | (min* M) = ((k --> 0 ) ^ q) | (min* M) & ((k --> 0 ) ^ q) | (min* M) = (k --> 0 ) ^ (q | mk) ) by A13, Th2, Th3;
then ( Sum (p | (min* M)) = (Sum (k --> 0 )) + (Sum (q | mk)) & Sum (k --> 0 ) = k * 0 ) by A10, Lm2, Lm4;
then ( mk + k <= mk & 1 <= k ) by A2, A3, A11, Th6, NAT_1:14;
hence contradiction by NAT_1:19; :: thesis: verum

end;

suppose min* M > k + (len q) ; :: thesis: contradiction

then reconsider mkL = (min* M) - (k + (len q)) as Element of NAT by NAT_1:21;
( dom ((k --> 0 ) ^ q) = (len (k --> 0 )) + (len q) & len (k --> 0 ) = dom (k --> 0 ) & len (((k --> 0 ) ^ q) ^ (k --> 1)) = (2 * k) + (len q) & min* M < len (((k --> 0 ) ^ q) ^ (k --> 1)) & dom (k --> 0 ) = k ) by A7, A8, AFINSQ_1:def 4, FUNCOP_1:19, XXREAL_0:1;
then ( min* M = (dom ((k --> 0 ) ^ q)) + mkL & mkL < ((2 * k) + (len q)) - (k + (len q)) ) by XREAL_1:11;
then ( (((k --> 0 ) ^ q) ^ (k --> 1)) | (min* M) = ((k --> 0 ) ^ q) ^ ((k --> 1) | mkL) & (k --> 1) | mkL = mkL --> 1 ) by Lm1, Th3;
then ( Sum (p | (min* M)) = (Sum ((k --> 0 ) ^ q)) + (Sum ((k --> 1) | mkL)) & Sum ((k --> 1) | mkL) = mkL * 1 & Sum ((k --> 0 ) ^ q) = (Sum (k --> 0 )) + (Sum q) & Sum (k --> 0 ) = k * 0 & 2 * (Sum (p | (min* M))) = min* M ) by A10, A11, Lm2, Lm4;
hence contradiction by A2, A7; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence min* { n where n is Element of NAT : ( 2 * (Sum (p | n)) = n & n > 0 ) } = (2 * k) + (len q) ; :: thesis: verum