Introduction to Go-Board - Part II
Jaros law Kotowicz, Yatsuka Nakamura · 1992
The scheme FinSeqDChoice deals with a non empty set A , a natural number B, and a binary predicate P , and states that: There exists a finite sequence f of elements of A such that len f = B and for every n such that n ∈ SegB holds P [n, fn] provided the parameters satisfy the following condition: • For every n such that n ∈ SegB there exists an element d of A such that P [n,d]. We now state several propositions: