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 ![](../FONT/kl-op.png)
f:
 ![](../FONT/dash.png)
 
. 
n:
. [prop]![](../FONT/kl-cl.png)
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![](../FONT/dot.png)
brouwer_prin_for_num_simpl{i:l}() ![](../FONT/if_big.png)
![](../FONT/eq.png)
 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