Nuprl Lemma : brouwer_prin_num_simplified

Nuprl Lemma : brouwer_prin_num_simplified_equiv

T must only consume finitely many elements of
the list before producing B
this T will be the witness for

f:

.

n:

. [prop]

given a list, T either produces an inr(Ax) saying
it needs to see more elements of the sequence to
produce b
Or, it produces b

The proof was once correct.
But after change of defns, it has to be redone

brouwer_prin_for_num_simpl{i:l}()

brouwer_prin_for_num_27_2{i:l}()

Proof not projected

Error : references
brouwer\_prin\_for\_num\_simpl\{i:l\}() \mLeftarrow{}{}\mRightarrow{} brouwer\_prin\_for\_num\_27\_2\{i:l\}() Date html generated: 2013_03_20-AM-11_02_14 Last ObjectModification: 2013_03_16-PM-01_18_05 Home Index