:: by Hiroshi Fujiwara , Hokuto Watari and Hiroaki Yamamoto

::

:: Received January 13, 2020

:: Copyright (c) 2020-2021 Association of Mizar Users

:: deftheorem defines Seq PRSUBSET:def 1 :

for x being FinSequence

for I being set holds Seq (x,I) = Seq (x | I);

for x being FinSequence

for I being set holds Seq (x,I) = Seq (x | I);

registration
end;

registration
end;

registration

let D be set ;

let x be D -valued FinSequence;

let i be Nat;

correctness

coherence

for b_{1} being FinSequence-like Function st b_{1} = x | i holds

b_{1} is D -valued ;

;

end;
let x be D -valued FinSequence;

let i be Nat;

correctness

coherence

for b

b

;

registration

let x be real-valued FinSequence;

let i be Nat;

correctness

coherence

for b_{1} being FinSequence-like Function st b_{1} = x | i holds

b_{1} is real-valued ;

;

end;
let i be Nat;

correctness

coherence

for b

b

;

definition

let x be REAL -valued FinSequence;

let a be Real;

end;
let a be Real;

pred x exist_subset_sum_eq a means :: PRSUBSET:def 2

ex I being set st

( I c= dom x & Sum (Seq (x,I)) = a );

ex I being set st

( I c= dom x & Sum (Seq (x,I)) = a );

:: deftheorem defines exist_subset_sum_eq PRSUBSET:def 2 :

for x being REAL -valued FinSequence

for a being Real holds

( x exist_subset_sum_eq a iff ex I being set st

( I c= dom x & Sum (Seq (x,I)) = a ) );

for x being REAL -valued FinSequence

for a being Real holds

( x exist_subset_sum_eq a iff ex I being set st

( I c= dom x & Sum (Seq (x,I)) = a ) );

LM010: for x being REAL -valued FinSequence ex Q being Function of [:(Seg (len x)),REAL:],BOOLEAN st

for i being Nat

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies Q . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies Q . (i,s) = FALSE ) )

proof end;

LM020: for x being REAL -valued FinSequence

for Q1, Q2 being Function of [:(Seg (len x)),REAL:],BOOLEAN st ( for i being Nat

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies Q1 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies Q1 . (i,s) = FALSE ) ) ) & ( for i being Nat

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies Q2 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies Q2 . (i,s) = FALSE ) ) ) holds

Q1 = Q2

proof end;

definition

let x be REAL -valued FinSequence;

ex b_{1} being Function of [:(Seg (len x)),REAL:],BOOLEAN st

for i being Nat

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies b_{1} . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b_{1} . (i,s) = FALSE ) )
by LM010;

uniqueness

for b_{1}, b_{2} being Function of [:(Seg (len x)),REAL:],BOOLEAN st ( for i being Nat

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies b_{1} . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b_{1} . (i,s) = FALSE ) ) ) & ( for i being Nat

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies b_{2} . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b_{2} . (i,s) = FALSE ) ) ) holds

b_{1} = b_{2}
by LM020;

end;
func Q_ex x -> Function of [:(Seg (len x)),REAL:],BOOLEAN means :defQ: :: PRSUBSET:def 3

for i being Nat

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies it . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies it . (i,s) = FALSE ) );

existence for i being Nat

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies it . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies it . (i,s) = FALSE ) );

ex b

for i being Nat

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies b

uniqueness

for b

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies b

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies b

b

:: deftheorem defQ defines Q_ex PRSUBSET:def 3 :

for x being REAL -valued FinSequence

for b_{2} being Function of [:(Seg (len x)),REAL:],BOOLEAN holds

( b_{2} = Q_ex x iff for i being Nat

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies b_{2} . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b_{2} . (i,s) = FALSE ) ) );

for x being REAL -valued FinSequence

for b

( b

for s being Real st 1 <= i & i <= len x holds

( ( x | i exist_subset_sum_eq s implies b

registration

let A be Subset of NAT;

let i be Nat;

let s be Real;

let f be Function of [:A,REAL:],BOOLEAN;

correctness

coherence

f . (i,s) is boolean ;

;

end;
let i be Nat;

let s be Real;

let f be Function of [:A,REAL:],BOOLEAN;

correctness

coherence

f . (i,s) is boolean ;

;

:: deftheorem defines _eq_ PRSUBSET:def 4 :

for a, b being object holds a _eq_ b = IFEQ (a,b,TRUE,FALSE);

for a, b being object holds a _eq_ b = IFEQ (a,b,TRUE,FALSE);

registration
end;

:: deftheorem defines _le_ PRSUBSET:def 5 :

for a, b being ExtReal holds a _le_ b = IFGT (a,b,FALSE,TRUE);

for a, b being ExtReal holds a _le_ b = IFGT (a,b,FALSE,TRUE);

registration
end;

Lemacik1: for x being REAL -valued FinSequence st 1 <= len x holds

dom (x | 1) = {1}

proof end;

theorem :: PRSUBSET:1

for s being Real

for x being REAL -valued FinSequence st 1 <= len x holds

(Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0)

for x being REAL -valued FinSequence st 1 <= len x holds

(Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0)

proof end;

LM040: for i, k, x being Nat

for I being set st I c= Seg k & k < x & x in Seg i holds

Sgm (I \/ {x}) = (Sgm I) ^ <*x*>

proof end;

theorem LM060: :: PRSUBSET:3

for x being REAL -valued FinSequence

for i being Nat

for I0 being set st I0 c= Seg i & Seg (i + 1) c= dom x holds

Seq ((x | (i + 1)),(I0 \/ {(i + 1)})) = (Seq ((x | i),I0)) ^ <*(x . (i + 1))*>

for i being Nat

for I0 being set st I0 c= Seg i & Seg (i + 1) c= dom x holds

Seq ((x | (i + 1)),(I0 \/ {(i + 1)})) = (Seq ((x | i),I0)) ^ <*(x . (i + 1))*>

proof end;

theorem LM090: :: PRSUBSET:5

for x being real-valued FinSequence

for i being Nat st x is positive & 1 <= i & i <= len x holds

( x | i is positive & x | i <> {} )

for i being Nat st x is positive & 1 <= i & i <= len x holds

( x | i is positive & x | i <> {} )

proof end;

theorem LM100: :: PRSUBSET:6

for x being real-valued FinSequence

for I being set st x is positive & I c= dom x & I <> {} holds

( Seq (x,I) is positive & Seq (x,I) <> {} )

for I being set st x is positive & I c= dom x & I <> {} holds

( Seq (x,I) is positive & Seq (x,I) <> {} )

proof end;

:: Recurrence Relation: Induction Case

theorem :: PRSUBSET:7

for x being REAL -valued FinSequence st x is positive holds

for i being Nat

for s being Real st 1 <= i & i < len x holds

(Q_ex x) . ((i + 1),s) = ((Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' ((Q_ex x) . (i,(s - (x . (i + 1))))))

for i being Nat

for s being Real st 1 <= i & i < len x holds

(Q_ex x) . ((i + 1),s) = ((Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' ((Q_ex x) . (i,(s - (x . (i + 1))))))

proof end;